PBLib – a library for encoding pseudo-Boolean constraints into CNF. (English) Zbl 1471.68261

Philipp, Tobias; Steinke, Peter

Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 9-16 (2015).

Summary: PBLib is an easy-to-use and efficient library, written in \(\mathrm {C}_{++}\), for translating pseudo-Boolean (PB) constraints into CNF. We have implemented fifteen different encodings of PB constraints. Our aim is to use efficient encodings, in terms of formula size and whether unit propagation maintains generalized arc consistency. Moreover, PBLib normalizes PB constraints and automatically uses a suitable encoder for the translation. We also support incremental strengthening for optimization problems, where the tighter bound is realized with few additional clauses, as well as conditions for PB constraints.
For the entire collection see [Zbl 1323.68009].

MSC:

68T20

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

BoolVar/PB; NiVER; npSolver; MiniSat; PBLib

References:

[1]	Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A parametric approach for smaller and better encodings of cardinality constraints. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 80–96. Springer, Heidelberg (2013) · Zbl 1432.68412
[2]	Frisch, A.M., Peugniez, T.J., Doggett, A.J., Nightingale, P.W.: Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings. Journal of Automated Reasoning 35 (2005) · Zbl 1109.68109
[3]	Bailleux, O.: Boolvar/PB 1.0 (2012). http://boolvar.sourceforge.net/
[4]	Belov, A., Janota, M., Lynce, I., Marques-Silva, J.: On computing minimal equivalent subformulas. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 158–174. Springer, Heidelberg (2012) · Zbl 06122837
[5]	Boros, E., Hammer, P.L.: Pseudo-Boolean optimization. Discrete Applied Mathematics 123(1–3), 155–225 (2002) · Zbl 1076.90032
[6]	Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Communications of the ACM 54(12), 92–103 (2011)
[7]	Chen, J.: A new SAT encoding of the at-most-one constraint. In: ModRef 2010 (2010)
[8]	Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463
[9]	Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191
[10]	Een, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2, 1–26 (2006) · Zbl 1116.68083
[11]	Großmann, P., Hölldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA/AIE 2012. LNCS, vol. 7345, pp. 166–175. Springer, Heidelberg (2012) · Zbl 06164661
[12]	Hölldobler, S., Manthey, N., Steinke, P.: A compact encoding of pseudo-boolean constraints into SAT. In: Glimm, B., Krüger, A. (eds.) KI 2012. LNCS, vol. 7526, pp. 107–118. Springer, Heidelberg (2012) · Zbl 06123279
[13]	Hölldobler, S., Nguyen, V.H.: On SAT-encodings of the at-most-one constraint. In: ModRef 2013 (2013)
[14]	Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: BDDs for pseudo-boolean constraints – revisited. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 61–75. Springer, Heidelberg (2011) · Zbl 1330.68098
[15]	Kautz, H., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) ECAI 1992, pp. 359–363. John Wiley & Sons Inc., New York (1992)
[16]	Kautz, H., Selman, B.: Pushing the envelope: planning, propositional logic, and stochastic search. In: AAAI 1996, pp. 1194–1201. MIT Press (1996)
[17]	Klieber, W., Kwon, G.: Efficient CNF encoding for selecting 1 from n objects. In: CFV 2007 (2007)
[18]	Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1–33 (2008) · Zbl 1154.68510
[19]	Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 102–117. Springer, Heidelberg (2013) · Zbl 06232564
[20]	Manthey, N., Philipp, T., Steinke, P.: A more compact translation of pseudo-boolean constraints into CNF such that generalized arc consistency is maintained. In: Lutz, C., Thielscher, M. (eds.) KI 2014. LNCS, vol. 8736, pp. 123–134. Springer, Heidelberg (2014) · Zbl 06465938
[21]	Manthey, N., Steinke, P.: npSolver - a SAT based solver for optimization problems. In: POS 2012 (2012)
[22]	Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Bloem, R., Sharygina, N. (eds.) FMCAD 2010, pp. 121–128 (2010)
[23]	Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 181–194. Springer, Heidelberg (2009) · Zbl 1247.68246
[24]	Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986) · Zbl 0636.68119
[25]	Rossi, F., Beek, P.V., Walsh, T.: Handbook of Constraint Programming. Elsevier Science Inc., New York (2006) · Zbl 1175.90011
[26]	Roussel, O., Manquinho, V.: Input/output format and solver requirements for the competitions of pseudo-Boolean solvers (2012)
[27]	Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005) · Zbl 1153.68488
[28]	Sorensson, N., Een, N.: MiniSat - a SAT solver with conflict-clause minimization. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS. Springer, Heidelberg (2005)
[29]	Subbarayan, S., Pradhan, D.K.: NiVER: non-increasing variable elimination resolution for preprocessing SAT instances. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005) · Zbl 1122.68618
[30]	Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983)