Advertisement

Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints

  • Carlos Ansótegui
  • Miquel Bofill
  • Jordi CollEmail author
  • Nguyen Dang
  • Juan Luis Esteban
  • Ian Miguel
  • Peter Nightingale
  • András Z. Salamon
  • Josep Suy
  • Mateu Villaret
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11802)

Abstract

Pseudo-Boolean (PB) constraints often have a critical role in constraint satisfaction and optimisation problems. Encoding PB constraints to SAT has proven to be an efficient approach in many applications, however care must be taken to encode them compactly and with good propagation properties. It has been shown that at-most-one (AMO) and exactly-one (EO) relations over subsets of the variables can be exploited in various encodings of PB constraints, improving their compactness and solving performance. In this paper we detect AMO and EO relations completely automatically and exploit them to improve SAT encodings that are based on Multi-Valued Decision Diagrams (MDDs). Our experiments show substantial reductions in encoding size and dramatic improvements in solving time thanks to automatic AMO and EO detection.

Keywords

Automatic CSP reformulation SAT Pseudo-Boolean At-most-one constraint 
This is a preview of subscription content, log in to check access.

References

  1. 1.
    Abío, I., Mayer-Eichberger, V., Stuckey, P.J.: Encoding linear constraints with implication chains to CNF. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 3–11. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23219-5_1CrossRefGoogle Scholar
  2. 2.
    Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-Boolean constraints. J. Artif. Intell. Res. 443–480 (2012).  https://doi.org/10.1613/jair.3653MathSciNetCrossRefGoogle Scholar
  3. 3.
    Ansótegui, C.: Complete SAT solvers for Many-Valued CNF Formulas. Ph.D. thesis, University of Lleida (2004)Google Scholar
  4. 4.
    Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1–25 (2018).  https://doi.org/10.1142/S0218213018400018CrossRefGoogle Scholar
  5. 5.
    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).  https://doi.org/10.1007/978-3-642-02777-2_19CrossRefzbMATHGoogle Scholar
  6. 6.
    Biere, A.: Lingeling. SAT Race (2010)Google Scholar
  7. 7.
    Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 285–301. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09284-3_22CrossRefGoogle Scholar
  8. 8.
    Bofill, M., Coll, J., Suy, J., Villaret, M.: Compact MDDs for pseudo-boolean constraints with at-most-one relations in resource-constrained scheduling problems. In: IJCAI, pp. 555–562 (2017).  https://doi.org/10.24963/ijcai.2017/78
  9. 9.
    Bofill, M., Palahí, M., Suy, J., Villaret, M.: Solving intensional weighted CSPs by incremental optimization with BDDs. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 207–223. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10428-7_17CrossRefzbMATHGoogle Scholar
  10. 10.
    Brucker, P., Drexl, A., Möhring, R., Neumann, K., Pesch, E.: Resource-constrained project scheduling: notation, classification, models, and methods. Eur. J. Oper. Res. 112(1), 3–41 (1999).  https://doi.org/10.1016/S0377-2217(98)00204-5CrossRefzbMATHGoogle Scholar
  11. 11.
    Darras, S., Dequen, G., Devendeville, L., Mazure, B., Ostrowski, R., Saïs, L.: Using Boolean Constraint Propagation for sub-clauses deduction. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 757–761. Springer, Heidelberg (2005).  https://doi.org/10.1007/11564751_59CrossRefzbMATHGoogle Scholar
  12. 12.
    De Causmaecker, P., Vanden Berghe, G.: A categorisation of nurse rostering problems. J. Sched. 14(1), 3–16 (2011).  https://doi.org/10.1007/s10951-010-0211-zCrossRefGoogle Scholar
  13. 13.
    Eén, N., Sorensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1–26 (2006). http://satassociation.org/jsat/index.php/jsat/article/view/18
  14. 14.
    Fourdrinoy, O., Grégoire, É., Mazure, B., Saïs, L.: Eliminating redundant clauses in SAT instances. In: Van Hentenryck, P., Wolsey, L. (eds.) CPAIOR 2007. LNCS, vol. 4510, pp. 71–83. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-72397-4_6CrossRefzbMATHGoogle Scholar
  15. 15.
    Gent, I.P., Jefferson, C., Miguel, I.: Minion: a fast scalable constraint solver. In: ECAI: European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 141, pp. 98–102. IOS Press (2006). http://www.booksonline.iospress.nl/Content/View.aspx?piid=1654
  16. 16.
    Han, B., Leblet, J., Simon, G.: Hard multidimensional multiple choice knapsack problems, an empirical study. Comput. Oper. Res. 37(1), 172–181 (2010).  https://doi.org/10.1016/j.cor.2009.04.006MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    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 (LNAI), vol. 7526, pp. 107–118. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33347-7_10CrossRefGoogle Scholar
  18. 18.
    Huang, J.: Universal booleanization of constraint models. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 144–158. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85958-1_10CrossRefGoogle Scholar
  19. 19.
    Joshi, S., Martins, R., Manquinho, V.: Generalized totalizer encoding for pseudo-boolean constraints. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 200–209. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23219-5_15CrossRefGoogle Scholar
  20. 20.
    Kellerer, H., Pferschy, U., Pisinger, D.: Multidimensional knapsack problems. In: Knapsack Problems, pp. 235–283. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24777-7_9CrossRefGoogle Scholar
  21. 21.
    Kolisch, R., Sprecher, A.: PSPLIB - a project scheduling problem library. Eur. J. Oper. Res. 96(1), 205–216 (1997).  https://doi.org/10.1016/S0377-2217(96)00170-1CrossRefzbMATHGoogle Scholar
  22. 22.
    Leyton-Brown, K., Shoham, Y.: A test suite for combinatorial auctions. In: Combinatorial Auctions, chap. 18, pp. 451–478. The MIT Press (2006)Google Scholar
  23. 23.
    Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver’. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09284-3_33CrossRefGoogle Scholar
  24. 24.
    Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74970-7_38CrossRefGoogle Scholar
  25. 25.
    Nightingale, P., Akgün, Ö., Gent, I.P., Jefferson, C., Miguel, I., Spracklen, P.: Automatically improving constraint models in Savile Row. Artif. Intell. 251, 35–61 (2017).  https://doi.org/10.1016/j.artint.2017.07.001MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Nightingale, P., Rendl, A.: Essence’ description. arXiv:1601.02865 (2016)
  27. 27.
    Vanhoucke, M., Maenhout, B.: NSPLib: a nurse scheduling problem library: a tool to evaluate (meta-)heuristic procedures. In: Brailsford, S., Harper, P. (eds.) Operational research for health policy: making better decisions, pp. 151–165. Peter Lang (2007)Google Scholar
  28. 28.
    Zhou, N.-F., Kjellerstrand, H.: The Picat-SAT compiler. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 48–62. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-28228-2_4CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Carlos Ansótegui
    • 1
  • Miquel Bofill
    • 2
  • Jordi Coll
    • 2
    Email author
  • Nguyen Dang
    • 3
  • Juan Luis Esteban
    • 4
  • Ian Miguel
    • 3
  • Peter Nightingale
    • 5
  • András Z. Salamon
    • 3
  • Josep Suy
    • 2
  • Mateu Villaret
    • 2
  1. 1.University of LleidaLleidaSpain
  2. 2.University of GironaGironaSpain
  3. 3.University of St AndrewsSt AndrewsUK
  4. 4.Technical University of CataloniaBarcelonaSpain
  5. 5.University of YorkYorkUK

Personalised recommendations

Cite paper

Buy options