Incremental Cardinality Constraints for MaxSAT
Maximum Satisfiability (MaxSAT) is an optimization variant of the Boolean Satisfiability (SAT) problem. In general, MaxSAT algorithms perform a succession of SAT solver calls to reach an optimum solution making extensive use of cardinality constraints. Many of these algorithms are non-incremental in nature, i.e. at each iteration the formula is rebuilt and no knowledge is reused from one iteration to another. In this paper, we exploit the knowledge acquired across iterations using novel schemes to use cardinality constraints in an incremental fashion. We integrate these schemes with several MaxSAT algorithms. Our experimental results show a significant performance boost for these algo- rithms as compared to their non-incremental counterparts. These results suggest that incremental cardinality constraints could be beneficial for other constraint solving domains.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Reflections on "Incremental Cardinality Constraints for MaxSAT"
To celebrate the first 25 years of the International Conference on Principles and Practice of Constraint Programming (CP) the editors invited the authors of the most cited paper of each year to write a commentary on thei…
IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses
Recently, a novel, MaxSAT-based method for error correction in quantum computing has been proposed that requires both incremental MaxSAT solving capabilities and support for XOR constraints, but no dedicated MaxSAT solve…
Solving Set Optimization Problems by Cardinality Optimization via Weak Constraints with an Application to Argumentation
Optimization - minimization or maximization - in the lattice of subsets is a frequent operation in Artificial Intelligence tasks. Examples are subset-minimal model-based diagnosis, nonmonotonic reasoning by means of circ…
Abstract ArgumentationUnsatisfiable Cores and Lower Bounding for Constraint Programming
Constraint Programming (CP) solvers typically tackle optimization problems by repeatedly finding solutions to a problem while placing tighter and tighter bounds on the solution cost. This approach is somewhat naive, espe…
DPO: Dynamic-Programming Optimization on Hybrid Constraints
In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literal-weighted CNF for…
Bayesian Inference