Proteus

Proteus: a hierarchical portfolio of solvers and transformations. In recent years, portfolio approaches to solving SAT problems and CSPs have become increasingly common. There are also a number of different encodings for representing CSPs as SAT instances. In this paper, we leverage advances in both SAT and CSP solving to present a novel hierarchical portfolio-based approach to CSP solving, which we call Proteus, that does not rely purely on CSP solvers. Instead, it may decide that it is best to encode a CSP problem instance into SAT, selecting an appropriate encoding and a corresponding SAT solver. Our experimental evaluation used an instance of Proteus that involved four CSP solvers, three SAT encodings, and six SAT solvers, evaluated on the most challenging problem instances from the CSP solver competitions, involving global and intensional constraints. We show that significant performance improvements can be achieved by Proteus obtained by exploiting alternative view-points and solvers for combinatorial problem-solving.


References in zbMATH (referenced in 10 articles )

Showing results 1 to 10 of 10.
Sorted by year (citations)

  1. Lindauer, Marius; van Rijn, Jan N.; Kotthoff, Lars: The algorithm selection competitions 2015 and 2017 (2019)
  2. Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
  3. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  4. Freuder, Eugene C.: Progress towards the Holy Grail (2018)
  5. Malone, Brandon; Kangas, Kustaa; Järvisalo, Matti; Koivisto, Mikko; Myllymäki, Petri: Empirical hardness of finding optimal Bayesian network structures: algorithm selection and runtime prediction (2018)
  6. Bischl, Bernd; Kerschke, Pascal; Kotthoff, Lars; Lindauer, Marius; Malitsky, Yuri; Fréchette, Alexandre; Hoos, Holger; Hutter, Frank; Leyton-Brown, Kevin; Tierney, Kevin; Vanschoren, Joaquin: ASlib: a benchmark library for algorithm selection (2016)
  7. Hurley, Barry; O’Sullivan, Barry; Allouche, David; Katsirelos, George; Schiex, Thomas; Zytnicki, Matthias; de Givry, Simon: Multi-language evaluation of exact solvers in graphical model discrete optimization (2016)
  8. Inala, Jeevana Priya; Singh, Rohit; Solar-Lezama, Armando: Synthesis of domain specific CNF encoders for bit-vector solvers (2016)
  9. Amadini, Roberto; Gabbrielli, Maurizio; Mauro, Jacopo: Why CP portfolio solvers are (under)utilized? issues and challenges (2015)
  10. Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014) ioport