Skip to main content
SpringerLink
Log in

Encoding Linear Constraints with Implication Chains to CNF

  • Conference paper
  • First Online:
Book cover Principles and Practice of Constraint Programming (CP 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9255))

Abstract

Linear constraints are the most common constraints occurring in combinatorial problems. For some problems which combine linear constraints with highly combinatorial constraints, the best solving method is translation to SAT. Translation of a single linear constraint to SAT is a well studied problem, particularly for cardinality and pseudo-Boolean constraints. In this paper we describe how we can improve encodings of linear constraints by taking into account implication chains in the problem. The resulting encodings are smaller and can propagate more strongly than separate encodings. We illustrate benchmarks where the encoding improves performance.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abio, I., Mayer-Eichberge, V., Stuckey, P.: Encoding linear constraints with implication chains to CNF. Tech. rep., University of Melbourne (2015). http://www.people.eng.unimelb.edu.au/pstuckey/papers/cp2015a.pdf

  2. Abío, I.: Solving hard industrial combinatorial problems with SAT. Ph.D. thesis, Technical University of Catalonia (UPC) (2013)

    Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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. (JAIR) 45, 443–480 (2012)

    MATH  Google Scholar 

  5. Abío, I., Stuckey, P.J.: Encoding linear constraints into SAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 75–91. Springer, Heidelberg (2014)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

    Google Scholar 

  8. Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Dutertre, B., de Moura, L.: The YICES SMT Solver. Tech. rep., Computer Science Laboratory, SRI International (2006). http://yices.csl.sri.com

  10. 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)

    Chapter  Google Scholar 

  11. Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation 2(1–4), 1–26 (2006)

    MATH  Google Scholar 

  12. Gent, I.P., Prosser, P., Smith, B.M.: A 0/1 encoding of the GACLex constraint for pairs of vectors. In: ECAI 2002 workshop W9: Modelling and Solving Problems with Constraints. University of Glasgow (2002)

    Google Scholar 

  13. Heule, M.J.H., Järvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201–215. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. de Moura, L., Bjorner, N.: Z3: An Efficient SMT Solver. Tech. rep., Microsoft Research, Redmond (2007). http://research.microsoft.com/projects/z3

  15. Ohrimenko, O., Stuckey, P., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357–391 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  16. Petit, T., Régin, J.-C., Beldiceanu, N.: A \(\Theta \)(n) bound-consistency algorithm for the increasing sum constraint. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 721–728. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Srinivasan, A., Ham, T., Malik, S., Brayton, R.: Algorithms for discrete function manipulation. In: 1990 IEEE International Conference on Computer-Aided Design, ICCAD 1990, pp. 92–95. Digest of Technical Papers (1990)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NICTA, Canberra, Australia

    Ignasi Abío, Valentin Mayer-Eichberger & Peter J. Stuckey

  2. University of New South Wales, Sydney, Australia

    Valentin Mayer-Eichberger

  3. University of Melbourne, Melbourne, Australia

    Peter J. Stuckey

Authors
  1. Ignasi Abío
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Valentin Mayer-Eichberger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter J. Stuckey
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ignasi Abío .

Editor information

Editors and Affiliations

  1. École Polytechnique de Montréal, Montréal, Québec, Canada

    Gilles Pesant

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Abío, I., Mayer-Eichberger, V., Stuckey, P.J. (2015). Encoding Linear Constraints with Implication Chains to CNF. In: Pesant, G. (eds) Principles and Practice of Constraint Programming. CP 2015. Lecture Notes in Computer Science(), vol 9255. Springer, Cham. https://doi.org/10.1007/978-3-319-23219-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23219-5_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23218-8

  • Online ISBN: 978-3-319-23219-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation