Ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver

Andre Abrame, Djamal Habet

Abstract


Branch and bound (BnB) solvers for Max-SAT count at each node of the search tree the number of disjoint inconsistent subsets to compute the lower bound. In the last ten years, important advances have been made regarding the lower bound computation. Unit propagation based methods have been introduced to detect inconsistent subsets and a resolution-like inference rules have been proposed which allow a more incremental lower bound computation. We present in this paper our solver Ahmaxsat, which uses these new methods and improves them in several ways. The main contributions of our solver over the state of the art are: a new unit propagation scheme which considers all the variable propagation sources; extended sets of patterns which increase the amount of learning performed by the solver;  a heuristic which modifies the order of application of the max-resolution rule when transforming inconsistent subset;  and a new inconsistent subset treatment method which improves the lower bound estimation.  We describe these four main contributions and we give a general overview of \ahmaxsat, with additional implementation details. Finally, we present the result of the experimental study we have conducted. We first evaluate the impact of each contribution on \ahmaxsat performances before comparing our solver to the current best performing BnB solvers. The obtained results confirm the ones of the Max-SAT Evaluation 2014 where \ahmaxsat was ranked first in three of the nine categories.

Keywords


Max-SAT; Branch and Bound; Max-Resoluton

Full Text:

PDF

References


Andre Abrame and Djamal Habet. Inference rules in local search for max-sat. In 24th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2012), pages 207 – 214, Athens, Greece, 07 november 2012.

Andre Abrame and Djamal Habet. Efficient application of max-sat resolution on inconsistent subsets. In Barry OSullivan, editor, Principles and Practice of Constraint Programming, 8656 of Lecture Notes in Computer Science, pages 92–107. Springer International Publishing, 2014.

Andre Abrame and Djamal Habet. Local max-resolution in branch and bound solvers for max-sat. In 26th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2014), pages 336–343, 2014.

Andre Abrame and Djamal Habet. Maintaining and handling all unit propagation reasons in exact max-sat solvers. In Proceedings of the Seventh Annual Symposium on Combinatorial Search, SOCS 2014, pages 2–9, 2014.

Andre Abrame and Djamal Habet. On the extension of learning for max-sat. In Proceedings of the Seventh Starting AI Researchers’ Symposium, STAIRS 2012, 241 of Frontiers in Artificial Intelligence and Applications, pages 11–20. IOS Press, 2014.

Teresa Alsinet, Felip Manya, and Jordi Planes. Improved branch and bound algorithms for max-sat. In Proceedings of the 6th International Conference on the Theory and Applications of Satisfiability Testing - SAT’03, 2003.

Teresa Alsinet, Felip Manya, and Jordi Planes. A max-sat solver with lazy data structures. In Christian Lematre, Carlos Reyes, and Jess Gonzlez, editors, Advances in Artificial Intelligence - IBERAMIA’04, 3315 of LNCS, pages 334–342. Springer Berlin / Heidelberg, 2004.

Carlos Ansotegui, Maria Luisa Bonet, and Jordi Levy. A new algorithm for weighted partial maxsat. In AAAI, pages 3–8, 2010.

Carlos Ansotegui and Joel Gabas. Solving (weighted) partial maxsat with ilp. In Carla P. Gomes and Meinolf Sellmann, editors, Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems - CPAIOR 2013, 7874 of Lecture Notes in Computer Science, pages 403–409. Springer, 2013.

Carlos Ansotegui, Maria Luisa Bonet, and Jordi Levy. Solving (weighted) partial maxsat through satisfiability testing. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 5584 of Lecture Notes in Computer Science, pages 427–440. Springer Berlin Heidelberg, 2009.

Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. JSAT, 7(2-3):59–64, 2010.

Maria Luisa Bonet, Jordi Levy, and Felip Manya. Resolution for max-sat. Artificial Intelligence, 171(8-9):606–618, 2007.

Shaowei Cai, Chuan Luo, John Thornton, and Kaile Su. Tailoring local search for partial maxsat. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, pages 2623–2629, 2014.

Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, pages 225–239, 2011.

N. Een and N. Sorensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT’03), 2919 of Lecture Notes in Computer Science, pages 502–518, Santa Margherita Ligure, Italy, 2003. Springer.

Eugene C. Freuder and Richard J. Wallace. Partial constraint satisfaction. Artificial Intelligence, 58(13):21–70, 1992.

Z. Fu. Extending the Power of Boolean Satisfiability Solvers: Techniques and Applications. PhD thesis, Princeton University, 2007.

Zhaohui Fu and Sharad Malik. On solving the partial max-sat problem. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 4121 of Lecture Notes in Computer Science, pages 252–265. Springer Berlin Heidelberg, 2006.

Carla Gomes, Willem-Jan van Hoeve, and Lucian Leahu. The power of semidefinite programming relaxations for max-sat. In J. Beck and Barbara Smith, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems - CPAIOR’06, 3990 of LNCS, pages 104–118. Springer Berlin / Heidelberg, 2006.

Pierre Hansen and Brigitte Jaumard. Algorithms for the maximum satisfiability problem. Computing, 44:279–303, 1990.

Federico Heras and Javier Larrosa. New inference rules for efficient max-sat solving. In Proceedings of the 21st national conference on Artificial intelligence - AAAI’06, 1, pages 68–73. AAAI Press, 2006.

Federico Heras, Javier Larrosa, and Albert Oliveras. Minimaxsat: A new weighted max-sat solver. In Joao Marques-Silva and Karem Sakallah, editors, Theory and Applications of Satisfiability Testing SAT 2007, 4501 of Lecture Notes in Computer Science, pages 41–55. Springer Berlin / Heidelberg, 2007.

Federico Heras, Javier Larrosa, and Albert Oliveras. Minimaxsat: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research - JAIR, 31:1–32, 2008.

Federico Heras and Joao Marques-Silva. Read-once resolution for unsatisfiability-based max-sat algorithms. In Proceedings of the Twenty-Second international joint conference on Artificial Intelligence - IJCAI’11, 1 of IJCAI’11, pages 572–577. AAAI Press, 2011.

J.N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15(3):359–383, 1995.

R. G. Jeroslow and J. Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.

Steve Joy, John Mitchell, and Brian Borchers. A branch and cut algorithm for max-sat and weighted max-sat. In Satisfiability Problem: Theory and Applications, volume 35 of DIMACS series on Discrete Mathematics and Theoretical Computer Science, pages 519–536. American Mathematical Society, 1997.

Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. Qmaxsat: A partial max-sat solver. JSAT, 8(1/2):95–100, 2012.

Adrian Kugel. Improved exact solver for the weighted max-sat problem. In Daniel LeBerre, editor, Pragmatics of SAT - POS’10, 8 of EPiC Series, pages 15–27, 2010.

Javier Larrosa and Federico Heras. Resolution in max-sat and its relation to local consistency in weighted csps. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence - IJCAI’05, pages 193–198. Morgan Kaufmann Publishers Inc., 2005.

Javier Larrosa, Federico Heras, and Simon de Givry. A logical approach to efficient max-sat solving. Artificial Intelligence, 172(23):204–233, 2008.

Chu Min Li, Felip Manya, Nouredine Mohamedou, and Jordi Planes. Exploiting cycle structures in max-sat. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 5584 of LNCS, pages 467–480. Springer Berlin / Heidelberg, 2009.

Chu Min Li, Felip Manya, and Jordi Planes. Exploiting unit propagation to compute lower bounds in branch and bound max-sat solvers. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 3709 of LNCS, pages 403–414. Springer Berlin / Heidelberg, 2005.

Chu Min Li, Felip Manya, and Jordi Planes. Detecting disjoint inconsistent subformulas for computing lower bounds for max-sat. In Proceedings of the 21st National Conference on Artificial Intelligence - AAAI 2006, pages 86–91. AAAI Press, 2006.

Chu Min Li, Felip Manya, and Jordi Planes. New inference rules for max-sat. Journal of Artificial Intelligence Research, 30:321–359, 2007.

Chu Min Li, Felip Manya, Nouredine Ould Mohamedou, and Jordi Planes. Resolution-based lower bounds in maxsat. Constraints, 15(4):456–484, 2010.

Vasco Manquinho, Joao Marques-Silva, and Jordi Planes. Algorithms for weighted boolean optimization. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 5584 of Lecture Notes in Computer Science, pages 495–508. Springer Berlin Heidelberg, 2009.

Joao Marques-Silva and K. A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, August 1999.

Joao Marques-Silva and Jordi Planes. Algorithms for maximum satisfiability using unsatisfiable cores. In Design, Automation and Test in Europe (DATE 2008), pages 408–413. IEEE, 2008.

Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference - DAC ’01, pages 530–535. ACM, 2001.

Rolf Niedermeier and Peter Rossmanith. New upper bounds for maximum satisfiability. Journal of Algorithms, 36(1):63 – 88, 2000.

Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994.

D. Pretolani. Efficiency and stability of hypergraph sat algorithms. In Proceedings of the DIMACS Challenge II, 1993.

Haiou Shen and Hantao Zhang. Study of lower bound functions for max-2-sat. In Deborah L. McGuinness and George Ferguson, editors, Proceedings of the 19th National Conference on Artificial Intelligence - AAAI 2004, AAAI’04, pages 185–190. AAAI Press, 2004.

Kevin Smyth, Holger Hoos, and Thomas Stutzle. Iterated robust tabu search for max-sat. In Yang Xiang and Brahim Chaib-draa, editors, Advances in Artificial Intelligence, 2671 of LNCS, pages 995–995. Springer Berlin / Heidelberg, 2003.

Dawn M. Strickland, Earl Barnes, and Joel S. Sokol. Optimal protein structure alignment using maximum cliques. Operations Research, 53(3):389–402, 2005.

Hans van Maaren and Linda van Norden. Sums of squares, satisfiability and maximum satisfiability. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT’05, 3569 of LNCS, pages 294–308. Springer Berlin / Heidelberg, 2005.

Richard Wallace and Eugene C. Freuder. Comparative studies of constraint satisfaction and davis-putnam algorithms for maximum satisfiability problems. In D. Johnson and M. Trick, editors, Cliques, Coloring and Satisfiability, 26, pages 587–615. American Mathematical Society, 1996.

Zhao Xing and Weixiong Zhang. Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence, 164(1-2):47 – 80, 2005.

Hui Xu, Rob A. Rutenbar, and Karem Sakallah. sub-sat: a formulation for relaxed boolean satisfiability with applications in routing. In Proceedings of the 2002 International Symposium on Physical Design - ISPD ’02, pages 182–187. ACM, 2002.

Mutsunori Yagiura and Toshihide Ibaraki. Efficient 2 and 3-flip neighborhood search algorithms for the max sat. In Wen-Lian Hsu and Ming-Yang Kao, editors, Proceedings of the 4th Annual International Conference on Computing and Combinatorics - COCOON ’98, 1449 of Lecture Notes in Computer Science, pages 105–116. Springer, 1998.


Refbacks

  • There are currently no refbacks.