Document Open Access Logo

The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets

Authors Mikoláš Janota , António Morgado , José Fragoso Santos , Vasco Manquinho

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.31.pdf
  • Filesize: 3.04 MB
  • 16 pages

Document Identifiers

Author Details

Mikoláš Janota
  • Czech Technical University in Prague, Czech Republic
António Morgado
  • INESC-ID Lisbon, Portugal
José Fragoso Santos
  • INESC-ID/IST, University of Lisbon, Portugal
Vasco Manquinho
  • INESC-ID/IST, University of Lisbon, Portugal

Funding

The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902. This scientific article is part of the RICAIP project that has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 857306. This work was supported by national funds through FCT, Fundação para a Ciência e a Tecnologia, under project UIDB/50021/2020, the project INFOCOS with reference PTDC/CCI-COM/32378/2017 and the project DOME with reference PTDC/CCI-COM/31198/2017.

Cite AsGet BibTex

Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho. The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.31

Abstract

The paper introduces the Seesaw algorithm, which explores the Pareto frontier of two given functions. The algorithm is complete and generalizes the well-known implicit hitting set paradigm. The first given function determines a cost of a hitting set and is optimized by an exact solver. The second, called the oracle function, is treated as a black-box. This approach is particularly useful in the optimization of functions that are impossible to encode into an exact solver. We show the effectiveness of the algorithm in the context of static solver portfolio selection. The existing implicit hitting set paradigm is applied to cost function and an oracle predicate. Hence, the Seesaw algorithm generalizes this by enabling the oracle to be a function. The paper identifies two independent preconditions that guarantee the correctness of the algorithm. This opens a number of avenues for future research into the possible instantiations of the algorithm, depending on the cost and oracle functions used.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Optimization algorithms
Keywords
  • implicit hitting sets
  • minimal hitting set
  • MaxSAT
  • optimization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz. Overview and analysis of the SAT challenge 2012 solver competition. Artif. Intell., 223, 2015. URL: https://doi.org/10.1016/j.artint.2015.01.002.
  2. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Computer Aided Verification - 23rd International Conference, CAV. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_14.
  3. Jacques F. Benders. Partitioning procedures for solving mixed-variables programming problems. Comput. Manag. Sci., 2(1):3-19, 2005. URL: https://doi.org/10.1007/s10287-004-0020-y.
  4. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Principles and Practice of Constraint Programming - CP. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  5. Jessica Davies and Fahiem Bacchus. Exploiting the power of MIP solvers in MaxSAT. In Theory and Applications of Satisfiability Testing (SAT), volume 7962. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_13.
  6. Erin Delisle and Fahiem Bacchus. Solving weighted CSPs by successive relaxations. In International Conference on Principles and Practice of Constraint Programming. Springer, 2013. Google Scholar
  7. Jan Elffers and Jakob Nordström. A cardinal improvement to pseudo-boolean solving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence. AAAI Press, 2020. URL: https://aaai.org/ojs/index.php/AAAI/article/view/5508.
  8. Katalin Fazekas, Fahiem Bacchus, and Armin Biere. Implicit hitting set algorithms for maximum satisfiability modulo theories. In International Joint Conference on Automated Reasoning. Springer, 2018. Google Scholar
  9. M. R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. Google Scholar
  10. Arthur M Geoffrion. Generalized Benders decomposition. Journal of optimization theory and applications, 10(4), 1972. Google Scholar
  11. LLC Gurobi Optimization. Gurobi optimizer reference manual, 2021. URL: http://www.gurobi.com.
  12. John N. Hooker and Greger Ottosson. Logic-based benders decomposition. Mathematical Programming, 96(1), 2003. Google Scholar
  13. Ching-Lai Hwang and Abu Syed Md. Masud. Multiple Objective Decision Making emdash Methods and Applications. Springer Berlin Heidelberg, 1979. URL: https://doi.org/10.1007/978-3-642-45511-7.
  14. Alexey Ignatiev, Mikoláš Janota, and João Marques-Silva. Quantified maximum satisfiability: A core-guided approach. In Theory and Applications of Satisfiability Testing (SAT), volume 7962. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_19.
  15. Alexey Ignatiev, António Morgado, and João Marques-Silva. Propositional abduction with implicit hitting sets. In ECAI 2016 - 22nd European Conference on Artificial Intelligence. IOS Press, 2016. URL: https://doi.org/10.3233/978-1-61499-672-9-1327.
  16. Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, and João Marques-Silva. Smallest MUS extraction with minimal hitting set dualization. In Principles and Practice of Constraint Programming. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23219-5_13.
  17. Alexey Ignatiev, Mikoláš Janota, and João Marques-Silva. Quantified maximum satisfiability. Constraints An Int. J., 21(2), 2016. URL: https://doi.org/10.1007/s10601-015-9195-9.
  18. Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In IJCAR (2), volume 12167 of Lecture Notes in Computer Science. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_29.
  19. Jan Jakubův and Josef Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018619.
  20. Jan Jakubuv and Josef Urban. Hammering Mizar by learning clause guidance. In ITP, volume 141 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  21. Mikoláš Janota, William Klieber, Joao Marques-Silva, and Edmund Clarke. Solving QBF with counterexample guided refinement. Artificial Intelligence, 234, 2016. URL: https://doi.org/10.1016/j.artint.2016.01.004.
  22. Mikoláš Janota and Joao Marques-Silva. Abstraction-based algorithm for 2QBF. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_19.
  23. Stasys Jukna. Exponential lower bounds for semantic resolution. In Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS, volume 39. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/10.
  24. Marius Lindauer, Holger H. Hoos, Frank Hutter, and Kevin Leyton-Brown. Selection and configuration of parallel portfolios. In Handbook of Parallel Constraint Reasoning. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-63516-3_15.
  25. João Marques-Silva, Josep Argelich, Ana Graça, and Inês Lynce. Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell., 62(3-4), 2011. URL: https://doi.org/10.1007/s10472-011-9233-2.
  26. Joao Marques-Silva, Alexey Ignatiev, and Antonio Morgado. Horn maximum satisfiability: Reductions, algorithms and applications. In EPIA Conference on Artificial Intelligence. Springer, 2017. Google Scholar
  27. Erick Moreno-Centeno and Richard M. Karp. The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Oper. Res., 61(2), 2013. URL: https://doi.org/10.1287/opre.1120.1139.
  28. Alexander Nadel. On optimizing a generic function in SAT. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020. IEEE, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_28.
  29. Eoin O'Mahony, Emmanuel Hebrard, Alan Holland, Conor Nugent, and Barry O'Sullivan. Using Case-based Reasoning in an Algorithm Portfolio for Constraint Solving. In Irish Conference on Artificial Intelligence and Cognitive Science, 2008. Google Scholar
  30. Christos H. Papadimitriou. Computational complexity. Academic Internet Publ., 2007. Google Scholar
  31. Mark Parker and Jennifer Ryan. Finding the minimum weight IIS cover of an infeasible system of linear inequalities. Annals of Mathematics and Artificial Intelligence, 17(1), 1996. Google Scholar
  32. James A Reggia, Dana S Nau, and Pearl Y Wang. Diagnostic expert systems based on a set covering model. International journal of man-machine studies, 19(5), 1983. Google Scholar
  33. Raymond Reiter. A theory of diagnosis from first principles. Artificial intelligence, 32(1), 1987. Google Scholar
  34. Mikoláš Janota and João Marques-Silva. On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell., 233, 2016. URL: https://doi.org/10.1016/j.artint.2016.01.002.
  35. Paul Saikko, Johannes Peter Wallner, and Matti Järvisalo. Implicit hitting set algorithms for reasoning beyond NP. In Principles of Knowledge Representation and Reasoning (KR). AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12812.
  36. Stephan Schulz. E - a brainiac theorem prover. AI Commun., 15(2-3), 2002. Google Scholar
  37. João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-131.
  38. Roni Stern, Meir Kalech, Alexander Feldman, and Gregory Provan. Exploring the duality in conflict-directed model-based diagnosis. In AAAI Conference on Artificial Intelligence, volume 26, 2012. Google Scholar
  39. Miguel Terra-Neves, Inês Lynce, and Vasco M. Manquinho. Introducing Pareto minimal correction subsets. In Theory and Applications of Satisfiability Testing - SAT. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_13.
  40. E. L. Ulungu and J. Teghem. Multi-objective combinatorial optimization problems: A survey. Journal of Multi-Criteria Decision Analysis, 3(2), 1994. URL: https://doi.org/10.1002/mcda.4020030204.
  41. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reason., 37(1-2), 2006. Google Scholar
  42. Lin Xu, Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res., 32, 2008. URL: https://doi.org/10.1613/jair.2490.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact