This paper introduces a new hybrid method for efficiently integrating Pseudo-Boolean (PB) constraints into generic SAT solvers in order to solve PB satisfiability and optimization problems. To achieve this, we adopt the cutting-plane technique to draw inferences among PB constraints and combine it with generic implication graph analysis for conflict-induced learning. Novel features of our approach include a light-weight and efficient hybrid learning and backjumping strategy for analyzing PB constraints and CNF clauses in order to simultaneously learn both a CNF clause and a PB constraint with minimum overhead and use both to determine the backtrack level. Several techniques for handling the original and learned PB constraints are introduced. Overall, our method benefits significantly from the pruning power of the learned PB constraints, while keeping the overhead of adding them into the problem low. In this paper, we also address two other methods for solving PB problems, namely integer linear programming and pre-processing to CNF SAT, and present a thorough comparison between them and our hybrid method. Experimental comparison of our method against other hybrid approaches is also demonstrated. Additionally, we provide details of the MiniSAT-based implementation of our solver Pueblo to enable the reader to construct a similar one.

References in zbMATH (referenced in 33 articles , 1 standard article )

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

1 2 next

  1. Devriendt, Jo; Gleixner, Ambros; Nordström, Jakob: Learn to relax: integrating (0-1) integer linear programming with pseudo-Boolean conflict-driven search (2021)
  2. Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
  3. De Wulf, Wolf; Bogaerts, Bart: \textsclp2pb: translating answer set programs into pseudo-Boolean theories (2020)
  4. Le Berre, Daniel; Marquis, Pierre; Wallon, Romain: On weakening strategies for PB solvers (2020)
  5. Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
  6. Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao: Iterative and core-guided maxsat solving: a survey and assessment (2013)
  7. Qi, Guilin; Du, Jianfeng: Reasoning with uncertain and inconsistent OWL ontologies (2012)
  8. Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L.: Haplotype inference with pseudo-Boolean optimization (2011)
  9. Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin: Equality saturation: a new approach to optimization (2011)
  10. Di Rosa, Emanuele; Giunchiglia, Enrico; Maratea, Marco: Solving satisfiability problems with preferences (2010)
  11. Manquinho, Vasco; Martins, Ruben; Lynce, Inês: Improving unsatisfiability-based algorithms for Boolean optimization (2010)
  12. Morgado, António; Marques-Silva, Joao: Combinatorial optimization solutions for the maximum quartet consistency problem (2010)
  13. Bailleux, Olivier; Boufkhad, Yacine; Roussel, Olivier: New encodings of pseudo-Boolean constraints into CNF (2009)
  14. Binshtok, M.; Brafman, R. I.; Domshlak, C.; Shiomony, S. E.: Generic preferences over subsets of structured objects (2009)
  15. Buchheim, Christoph; Rinaldi, Giovanni: Terse integer linear programs for Boolean optimization (2009)
  16. Gebser, Martin; Kaminski, Roland; Kaufmann, Benjamin; Schaub, Torsten: On the implementation of weight constraint rules in conflict-driven ASP solvers (2009)
  17. Kovalev, Roman; Lysikov, Nikolay; Mikheev, Gennady; Pogorelov, Dmitry; Simonov, Vitaly; Yazykov, Vladislav; Zakharov, Sergey; Zharov, Ilya; Goryacheva, Irina; Soshenkov, Sergey; Torskaya, Elena: Freight car models and their computer-aided dynamic analysis (2009)
  18. Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi: Algorithms for weighted Boolean optimization (2009)
  19. Heras, Federico; Larrosa, Javier; de Givry, Simon; Schiex, Thomas: 2006 and 2007 Max-SAT evaluations: contributed instances (2008)
  20. Heras, F.; Larrosa, J.; Oliveras, A.: Minimaxsat: an efficient weighted Max-SAT solver (2008)

1 2 next