Algorithms for the maximum satisfiability problem

Pierre Hansen; Brigitte Jaumard

doi:10.1007/bf02241270

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

Fundamenta Informaticae ◽

10.3233/fi-2020-1974 ◽

2020 ◽

Vol 176 (3-4) ◽

pp. 271-297

Author(s):

Mario Alviano ◽

Carmine Dodaro

Keyword(s):

State Of The Art ◽

Answer Set Programming ◽

Efficient Algorithms ◽

Satisfiability Problem ◽

Core Analysis ◽

Stable Model ◽

Maximum Satisfiability ◽

Model Search ◽

Unsatisfiable Core ◽

Stable Models

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

Download Full-text

Boosting branch-and-bound MaxSAT solvers with clause learning

AI Communications ◽

10.3233/aic-210178 ◽

2021 ◽

pp. 1-21

Author(s):

Chu-Min Li ◽

Zhenxing Xu ◽

Jordi Coll ◽

Felip Manyà ◽

Djamal Habet ◽

...

Keyword(s):

Experimental Investigation ◽

Combinatorial Optimization ◽

Problem Solving ◽

Branch And Bound ◽

Real World ◽

Optimization Problems ◽

Satisfiability Problem ◽

Maximum Satisfiability ◽

Combinatorial Optimization Problems ◽

Clause Learning

The Maximum Satisfiability Problem, or MaxSAT, offers a suitable problem solving formalism for combinatorial optimization problems. Nevertheless, MaxSAT solvers implementing the Branch-and-Bound (BnB) scheme have not succeeded in solving challenging real-world optimization problems. It is widely believed that BnB MaxSAT solvers are only superior on random and some specific crafted instances. At the same time, SAT-based MaxSAT solvers perform particularly well on real-world instances. To overcome this shortcoming of BnB MaxSAT solvers, this paper proposes a new BnB MaxSAT solver called MaxCDCL. The main feature of MaxCDCL is the combination of clause learning of soft conflicts and an efficient bounding procedure. Moreover, the paper reports on an experimental investigation showing that MaxCDCL is competitive when compared with the best performing solvers of the 2020 MaxSAT Evaluation. MaxCDCL performs very well on real-world instances, and solves a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best performing MaxSAT solvers, solves the highest number of instances of a collection from all the MaxSAT evaluations held so far.

Download Full-text