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
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11802)


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.


Automatic CSP reformulation SAT Pseudo-Boolean At-most-one constraint 


  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). 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). 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). 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). 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). 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).
  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). 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). 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). Scholar
  12. 12.
    De Causmaecker, P., Vanden Berghe, G.: A categorisation of nurse rostering problems. J. Sched. 14(1), 3–16 (2011). Scholar
  13. 13.
    Eén, N., Sorensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2, 1–26 (2006).
  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). 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).
  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). 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). 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). 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). Scholar
  20. 20.
    Kellerer, H., Pferschy, U., Pisinger, D.: Multidimensional knapsack problems. In: Knapsack Problems, pp. 235–283. Springer, Heidelberg (2004). Scholar
  21. 21.
    Kolisch, R., Sprecher, A.: PSPLIB - a project scheduling problem library. Eur. J. Oper. Res. 96(1), 205–216 (1997). 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). 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). 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). 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). 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