Understanding the power of Max-SAT resolution through UP-resilience

Mohamed Sami Cherif (1) , Djamal Habet (1) , André Abrame (2)

1 COALA - COntraintes, ALgorithmes et Applications
2 Logike

Input: a formula Φ in Conjunctive Normal Form (CNF) Output: the maximum (resp. minimum) number of satisfied (resp. falsified) clauses in Φ over all possible variable assignments Branch & Bound (BnB) for Max-SAT Binary search algorithm which maintains and constantly updates two values : Upper Bound (UB): value of the best known solution Lower Bound (LB): estimation of the best accessible solution Cut: if LB ≥ UB then backtrack

Domaines: Intelligence artificielle [cs.AI]

Mohamed Sami Cherif, Djamal Habet, André Abrame. Understanding the power of Max-SAT resolution through UP-resilience. Thirtieth International Joint Conference on Artificial Intelligence (IJCAI-21), Aug 2021, Montreal-themed Virtual Reality, Canada. ⟨hal-03334479⟩