×

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
Cited 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

Cited 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
all top 5

Cited in 11 Serials

5 Journal of Satisfiability, Boolean Modeling and Computation
4 Constraints
2 Artificial Intelligence
2 The Journal of Artificial Intelligence Research (JAIR)
2 Multibody System Dynamics
1 AI Communications
1 Annals of Operations Research
1 Mathematical Methods of Operations Research
1 Fundamenta Informaticae
1 OR Spectrum
1 Logical Methods in Computer Science
all top 5

Cited in 7 Fields

24 Computer science (68-XX)
10 Operations research, mathematical programming (90-XX)
3 Biology and other natural sciences (92-XX)
2 Mathematical logic and foundations (03-XX)
1 Mechanics of particles and systems (70-XX)
1 Mechanics of deformable solids (74-XX)
1 Game theory, economics, finance, and other social and behavioral sciences (91-XX)

Citations by Year