Abstract
In this paper we answer the open question for the existence of a more compact encoding from Pseudo-Boolean constraints into CNF that maintains generalized arc consistency by unit propagation, formalized by Bailleux et al. in [21]. In contrast to other encodings our approach is defined in an abstract way and we present a concrete instantiation, resulting in a space complexity of \(\mathcal{O}(n^2 \text{\,log}^2(n)\text{\,log}(w_{\mathsf{max}}))\) clauses in contrast to \(\mathcal{O}(n^3 \text{\,log}(n)\text{\,log}(w_{\mathsf{max}}))\) clauses generated by the previously best known encoding that maintains generalized arc consistency.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-Boolean constraints. JAIR 45, 443–480 (2012)
Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann (ed.) [15], pp. 167–180
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)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): IOS Press, Amsterdam (2009)
Boros, E., Hammer, P.L.: Pseudo-boolean optimization. DAM 123(1-3), 155–225 (2002)
Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. CACM 54(12), 92–103 (2011)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. CACM 5(7), 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM 7(3), 201–215 (1960)
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)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. JSAT 2, 1–26 (2006)
Hölldobler, S., Manthey, N., Saptawijaya, A.: Improving resource-unaware SAT solvers. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 519–534. Springer, Heidelberg (2010)
Kautz, H., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) ECAI 1992, pp. 359–363. John Wiley & Sons, Inc., New York (1992)
Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: AAAI 1996, pp. 1194–1201. MIT Press (1996)
Kullmann, O. (ed.): SAT 2009. LNCS, vol. 5584. Springer, Heidelberg (2009)
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. JAR 40(1), 1–33 (2008)
Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102–117. Springer, Heidelberg (2013)
Manthey, N., Steinke, P.: npSolver – A SAT based solver for optimization problems. In: POS 2012 (2012)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001, pp. 530–535. ACM, New York (2001)
Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Bloem, R., Sharygina, N. (eds.) FMCAD 2010, pp. 121–128 (2010)
Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-Boolean constraints into CNF. In: Kullmann (ed.) [15], pp. 181–194
Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986)
Rossi, F., Beek, P.v., Walsh, T.: Handbook of Constraint Programming. Elsevier Science Inc., New York (2006)
Roussel, O., Manquinho, V.: Pseudo-Boolean and cardinality constraints. In: Biere, et al. (eds.) [5]
Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Manthey, N., Philipp, T., Steinke, P. (2014). 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: Advances in Artificial Intelligence. KI 2014. Lecture Notes in Computer Science(), vol 8736. Springer, Cham. https://doi.org/10.1007/978-3-319-11206-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-11206-0_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11205-3
Online ISBN: 978-3-319-11206-0
eBook Packages: Computer ScienceComputer Science (R0)