×

Pueblo

swMATH ID: 743
Software Authors: Sheini, Hossein M.; Sakallah, Karem A.
Description: 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.
Homepage: http://www.cril.univ-artois.fr/PB06/papers/pueblo15.pdf
Keywords: satisfiability; inference-based learning; integer linear programming; CDCL; cutting plane learning
Related Software: MiniSat; Chaff; Sat4j; PBS; PicoSAT; MaxSolver; MiniMaxSat; Open-WBO; Gurobi; DIMACS; UBCSAT; SATIRE; OPBDP; CPLEX; MIPLIB; clasp; RPOLY; CP-nets; SCIP; ASPTools
Referenced in: 33 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Pueblo: a hybrid pseudo-Boolean SAT solver. Zbl 1116.68090
Sheini, Hossein M.; Sakallah, Karem A.
2006
all top 5

Referenced by 84 Authors

5 Marques-Silva, João P.
4 Heras, Federico
4 Manquinho, Vasco M.
3 de Givry, Simon
3 Larrosa, Javier
2 Le Berre, Daniel
2 Lynce, Inês
2 Morgado, António
2 Oliveras, Albert
2 Planes, Jordi
2 Roussel, Olivier
2 Schiex, Thomas
2 Wallon, Romain
1 Bailleux, Olivier
1 Binshtok, M.
1 Bogaerts, Bart
1 Boufkhad, Yacine
1 Brafman, Ronen I.
1 Buchheim, Christoph
1 Carr, Eric
1 De Wulf, Wolf
1 Devriendt, Jo
1 Di Rosa, Emanuele
1 Domshlak, Carmel
1 Du, Jianfeng
1 East, Deborah
1 Fuhs, Carsten
1 Gebser, Martin
1 Giesl, Jürgen
1 Giunchiglia, Enrico
1 Gleixner, Ambros M.
1 Gómez Bofill, Walter
1 Goryacheva, Irina Georgievna
1 Gosavi, Abhijit
1 Graça, Ana
1 Iakhiaev, Mikhail
1 Kahraman, Aykut F.
1 Kaminski, Roland
1 Kaufmann, Benjamin
1 Kohler, Timothy A.
1 Kovalev, Roman
1 Kresl, James
1 Kyrillidis, Anastasios
1 Lerner, Sorin
1 Liffiton, Mark H.
1 Lysikov, Nikolay
1 Maratea, Marco
1 Markov, Igor L.
1 Marquis, Pierre
1 Martins, Ruben
1 Middeldorp, Aart
1 Mikheev, Gennady
1 Mikitiuk, Artur
1 Nieuwenhuis, Robert
1 Nordström, Jakob
1 Oliveira, Arlindo L.
1 Ozkaya, Emrah
1 Pogorelov, Dmitry
1 Qi, Guilin
1 Ramani, Arathi
1 Rinaldi, Giovanni
1 Sakallah, Karem A.
1 Sánchez, Martì
1 Schaub, Torsten H.
1 Schneider-Kamp, Peter
1 Sheini, Hossein M.
1 Shiomony, S. E.
1 Shrivastava, Anshumali
1 Simonov, Vitaly
1 Soshenkov, Sergey
1 Stepp, Michael
1 Tate, Ross
1 Tatlock, Zachary
1 Thiemann, René
1 Torskaya, Elena
1 Truszczyński, Mirosław
1 Van West, Carla
1 Vardi, Moshe Ya’akov
1 Wilshusen, Richard H.
1 Yazykov, Vladislav
1 Zakharov, Sergeĭ Viktorovich
1 Zankl, Harald
1 Zhang, Zhiwei
1 Zharov, Ilya

Referencing Publications by Year