Core-Guided Binary Search Algorithms for Maximum Satisfiability

Authors

  • Federico Heras University College Dublin
  • Antonio Morgado University College Dublin
  • Joao Marques-Silva University College Dublin

DOI:

https://doi.org/10.1609/aaai.v25i1.7822

Abstract

Several MaxSAT algorithms based on iterative SAT solving have been proposed in recent years. These algorithms are in general the most efficient for real-world applications. Existing data indicates that, among MaxSAT algorithms based on iterative SAT solving, the most efficient ones are core-guided, i.e. algorithms which guide the search by iteratively computing unsatisfiable subformulas (or cores). For weighted MaxSAT, core-guided algorithms exhibit a number of important drawbacks, including a possibly exponential number of iterations and the use of a large number of auxiliary variables. This paper develops two new algorithms for (weighted) MaxSAT that address these two drawbacks. The first MaxSAT algorithm implements core-guided iterative SAT solving with binary search. The second algorithm extends the first one by exploiting disjoint cores. The empirical evaluation shows that core-guided binary search is competitive with current MaxSAT solvers.

Downloads

Published

2011-08-04

How to Cite

Heras, F., Morgado, A., & Marques-Silva, J. (2011). Core-Guided Binary Search Algorithms for Maximum Satisfiability. Proceedings of the AAAI Conference on Artificial Intelligence, 25(1), 36-41. https://doi.org/10.1609/aaai.v25i1.7822

Issue

Section

Constraints, Satisfiability, and Search