On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving

Ruben Martins, Saurabh Joshi, Vasco Manquinho, Inês Lynce

Abstract


In recent years, unsatisfiability-based algorithms have become prevalent as state of the art for solving industrial instances of Maximum Satisfiability (MaxSAT). These algorithms perform a succession of unsatisfiable SAT solver calls until an optimal solution is found. In several of these algorithms, cardinality or pseudo-Boolean constraints are extended between iterations. However, in most cases, the formula provided to the SAT solver in each iteration must be rebuilt and no knowledge is reused from one iteration to the next.
This paper describes how to implement incremental unsatisfiability-based algorithms for MaxSAT. In particular, we detail and analyze our implementation of the MSU3 algorithm in the OPENWBO framework that performed remarkably well in the MaxSAT Evaluation of 2014. Furthermore, we also propose to extend incrementality to weighted MaxSAT through an incremental encoding of pseudo-Boolean constraints. The experimental results show that the performance of MaxSAT algorithms can be greatly improved by exploiting the learned information and maintaining the internal state of the SAT solver between iterations. Finally, the proposed incremental encodings of cardinality and pseudo-Boolean constraints are not exclusive for MaxSAT usage and can be used in other domains.


Keywords


MAX-SAT; Incremental Solving; CNF Encodings;

Full Text:

PDF

References


http://maxsat.ia.udl.cat/. Last accessed on 12th December 2014.

http://sat.inesc-id.pt/open-wbo/. Last accessed on 12th December 2014.

Ignasi Ab´ıo and Peter J. Stuckey. Conflict Directed Lazy Decomposition. In Michela Milano, editor, Principles and Practice of Constraint Programming, 7514 of LNCS, pages 70–85. Springer, 2012.

Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiabilitybased optimization in clasp. In Agostino Dovier and V´ıtor Santos Costa, editors, International

Conference on Logic Programming, 17 of LIPIcs, pages 211–221. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.

Carlos Ans´otegui, Maria Luisa Bonet, Joel Gab`as, and Jordi Levy. Improving WPM2 for (Weighted) Partial MaxSAT. In Principles and Practice of Constraint Programming, 8124 of LNCS, pages 117–132. Springer, 2013.

Carlos Ans´otegui, Maria Luisa Bonet, and Jordi Levy. Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In Kullmann [34], pages 427–440.

Carlos Ans´otegui, Maria Luisa Bonet, and Jordi Levy. A New Algorithm for Weighted Partial MaxSAT. In Maria Fox and David Poole, editors, AAAI Conference on Artificial Intelligence. AAAI Press, 2010.

Josep Argelich, Daniel Le Berre, Inˆes Lynce, Jo˜ao Marques-Silva, and Pascal Rapicault. Solving Linux Upgradeability Problems Using Boolean Optimization. In Workshop on Logics for Component Configuration, pages 11–22, 2010.

Roberto As´ın and Robert Nieuwenhuis. Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, pages 1–21, 2012.

Roberto As´ın, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodr´ıguez-Carbonell. Cardinality Networks: a theoretical and empirical study. Constraints, 16(2):195–221, 2011.

Gilles Audemard, Jean-Marie Lagniez, and Laurent Simon. Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In Matti J¨arvisalo and Allen Van Gelder, editors, International Conference on Theory and Applications of Satisfiability Testing, 7962 of LNCS, pages 309–317. Springer, 2013.

Olivier Bailleux and Yacine Boufkhad. Efficient CNF Encoding of Boolean Cardinality Constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming, 2833 of LNCS, pages 108–122. Springer, 2003.

Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New Encodings of Pseudo-Boolean Constraints into CNF. In Kullmann [34], pages 181–194.

Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. www.SMT-LIB.org.

Markus B¨uttner and Jussi Rintanen. Satisfiability Planning with Constraints on the Number of Actions. In Susanne Biundo, Karen L. Myers, and Kanna Rajan, editors, International Conference on Automated Planning and Scheduling, pages 292–299. AAAI Press, 2005.

Yibin Chen, Sean Safarpour, Jo˜ao Marques-Silva, and Andreas G. Veneris. Automated Design Debugging With Maximum Satisfiability. IEEE Transactions on CAD of Integrated Circuits and Systems, 29(11):1804–1817, 2010.

Alessandro Cimatti and Roberto Sebastiani, editors. International Conference on Theory and Applications of Satisfiability Testing, 7317 of LNCS. Springer, 2012.

Romuald Debruyne. Arc-Consistency in Dynamic CSPs Is No More Prohibitive. In International Conference on Tools with Artificial Intelligence, pages 299–307. IEEE, 1996.

Rina Dechter and Avi Dechter. Belief Maintenance in Dynamic Constraint Networks. In Howard E. Shrobe, Tom M. Mitchell, and Reid G. Smith, editors, AAAI Conference on Artificial Intelligence, pages 37–42. AAAI Press / The MIT Press, 1988.

Bruno Dutertre and Leonardo Mendonc¸a de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, 4144 of LNCS, pages 81–94. Springer, 2006.

Niklas E´en and Niklas S¨orensson. An Extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, International Conference on Theory and Applications of Satisfiability Testing, 2919 of LNCS, pages 502–518. Springer, 2003.

Niklas E´en and Niklas S¨orensson. Temporal induction by incremental SAT solving. Electronic Notes in Theoretical Computer Science, 89(4):543–560, 2003.

Niklas E´en and Niklas S¨orensson. Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2:1–26, 2006.

Zhaohui Fu and Sharad Malik. On Solving the Partial MAX-SAT Problem. In Armin Biere and Carla P. Gomes, editors, International Conference on Theory and Applications of Satisfiability Testing, 4121 of LNCS, pages 252–265. Springer, 2006.

Ana Grac¸a, Inˆes Lynce, Jo˜ao Marques-Silva, and Arlindo L. Oliveira. Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. In Katsuhisa Horimoto, Masahiko Nakatsui, and Nikolaj Popov, editors, Algebraic and Numeric Biology, 6479 of LNCS, pages 38–56. Springer, 2010.

Federico Heras, Ant´onio Morgado, and Jo˜ao Marques-Silva. Core-Guided Binary Search Algorithms for Maximum Satisfiability. In Wolfram Burgard and Dan Roth, editors, AAAI Conference on Artificial Intelligence. AAAI Press, 2011.

Steffen H¨olldobler, Norbert Manthey, and Peter Steinke. A Compact Encoding of Pseudo-Boolean Constraints into SAT. In Birte Glimm and Antonio Kr¨uger, editors, KI 2013: Advances in Artificial Intelligence, 7526 of LNCS, pages 107–118. Springer, 2012.

John N. Hooker. Solving the incremental satisfiability problem. Journal of Logic Programming, 15(1&2):177–186, 1993.

Alexey Ignatiev, Ant´onio Morgado, Vasco Manquinho, Inˆes Lynce, and Jo˜ao Marques-Silva. Progression in Maximum Satisfiability. In Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan, editors, European Conference on Artificial Intelligence, 263 of Frontiers in Artificial Intelligence and Applications, pages 453–458. IOS Press, 2014.

Manu Jose and Rupak Majumdar. Cause clue clauses: error localization using maximum satisfiability. In Mary W. Hall and David A. Padua, editors, Programming Language Design and Implementation, pages 437–446. ACM, 2011.

Saurabh Joshi and Daniel Kroening. Property-Driven Fence Insertion using Reorder Bounded Model Checking. CoRR, abs/1407.7443, 2014. http://arxiv.org/abs/1407.7443.

Serdar Kadioglu, Yuri Malitsky, and Meinolf Sellmann. Non-Model-Based Search Guidance for Set Partitioning Problems. In J¨org Hoffmann and Bart Selman, editors, AAAI Conference on Artificial Intelligence. AAAI Press, 2012.

Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, 8(1/2):95–100, 2012.

Oliver Kullmann, editor. International Conference on Theory and Applications of Satisfiability Testing, 5584 of LNCS. Springer, 2009.

Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):59–6, 2010.

Chu Min Li and Felip Many`a. MaxSAT, Hard and Soft Constraints. In Handbook of Satisfiability, pages 613–631. IOS Press, 2009.

Mark H. Liffiton and Karem A. Sakallah. Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints. Journal Automated Reasoning, 40(1):1–33, 2008.

Florian Lonsing and Uwe Egly. Incremental QBF solving. In O’Sullivan [54], pages 514–530.

Yogesh S. Mahajan, Zhaohui Fu, and Sharad Malik. Zchaff2004: An efficient sat solver. In Holger H. Hoos and David G. Mitchell, editors, International Conference on Theory and Applications of Satisfiability Testing, 3542 of LNCS, pages 360–375. Springer, 2004.

Panagiotis Manolios and Vasilis Papavasileiou. Pseudo-Boolean Solving by incremental translation to SAT. In Per Bjesse and Anna Slobodov´a, editors, International Conference on Formal Methods in Computer-Aided Design, pages 41–45. FMCAD Inc., 2011.

Vasco Manquinho, Joao Marques-Silva, and Jordi Planes. Algorithms for Weighted Boolean Optimization. In Kullmann [34], pages 495–508.

Paolo Marin, Christian Miller, Matthew D. T. Lewis, and Bernd Becker. Verification of partial designs using incremental QBF solving. In Wolfgang Rosenstiel and Lothar Thiele, editors, Design, Automation, and Test in Europe Conference, pages 623–628. IEEE, 2012.

Jo˜ao Marques-Silva, Josep Argelich, Ana Grac¸a, and Inˆes Lynce. Boolean lexicographic optimization: algorithms & applications. Annals of Mathematics and Artificial Intelligence, 62(3-4):317–343, 2011.

Jo˜ao Marques-Silva and Jordi Planes. On Using Unsatisfiability for Solving Maximum Satisfiability. CoRR, abs/0712.1097, 2007. http://arxiv.org/abs/0712.1097.

Ruben Martins, Saurabh Joshi, Vasco Manquinho, and Inˆes Lynce. Incremental Cardinality Constraints for MaxSAT. In O’Sullivan [54], pages 531–548.

Ruben Martins, Vasco Manquinho, and Inˆes Lynce. Parallel Search for Maximum Satisfiability. AI Communications, 25(2):75–95, 2012.

Ruben Martins, Vasco Manquinho, and Inˆes Lynce. Open-WBO: a Modular MaxSAT Solver. In C. Sinz and U. Egly, editors, International Conference on Theory and Applications of Satisfiability Testing, 8561 of LNCS, pages 438–445. Springer, 2014.

A. Morgado, F. Heras, M. Liffiton, J. Planes, and J. Marques-Silva. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 18(4):478–534, 2013.

Ant´onio Morgado, Carmine Dodaro, and Jo˜ao Marques-Silva. Core-Guided MaxSAT with Soft Cardinality Constraints. In O’Sullivan [54], pages 564–573.

Ant´onio Morgado, Federico Heras, and Jo˜ao Marques-Silva. Improvements to Core-Guided Binary Search for MaxSAT. In Cimatti and Sebastiani [17], pages 284–297.

Alexander Nadel and Vadim Ryvchin. Efficient SAT Solving under Assumptions. In Cimatti and Sebastiani [17], pages 242–255.

Nina Narodytska and Fahiem Bacchus. Maximum Satisfiability Using Core-Guided MaxSAT Resolution. In AAAI Conference on Artificial Intelligence, pages 2717–2723. AAAI Press, 2014.

Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, and Hiroshi Fujita. Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. In International Conference on Tools with Artificial Intelligence, pages 9 – 17. IEEE, 2013.

Barry O’Sullivan, editor. Principles and Practice of Constraint Programming, 8656 of LNCS. Springer, 2014.

Sven Reimer, Matthias Sauer, Tobias Schubert, and Bernd Becker. Incremental Encoding and Solving of Cardinality Constraints. In Franck Cassez and Jean-Francois Raskin, editors, Automated Technology for Verification and Analysis, 8837 of LNCS, pages 297–313. Springer, 2014.

Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming, 3709 of LNCS, pages 827–831. Springer, 2005.

Ofer Strichman. Pruning Techniques for the SAT-Based Bounded Model Checking Problem. In Tiziana Margaria and Thomas F. Melham, editors, Correct Hardware Design and Verification Methods, 2144 of LNCS, pages 58–70. Springer, 2001.

Joost P. Warners. A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2):63–69, 1998.

Jesse Whittemore, Joonyoung Kim, and Karem A. Sakallah. SATIRE: A New Incremental Satisfiability Engine. In Design Automation Conference, pages 542–545. ACM, 2001.


Refbacks

  • There are currently no refbacks.

Comments on this article

View all comments