Document Open Access Logo

Constraint Propagation and Explanation over Novel Types by Abstract Compilation

Authors Graeme Gange, Peter J. Stuckey

PDF

File

Thumbnail PDF
PDF
OASIcs.ICLP.2016.13.pdf
  • Filesize: 0.64 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • constraint programming
  • program synthesis
  • program analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The appeal of constraint programming (CP) lies in compositionality – the ability to mix and match constraints as needed. However, this flexibility typically does not extend to the types of variables. Solvers usually support only a small set of pre-defined variable types, and extending this is not typically a simple exercise: not only must the solver engine be updated, but then the library of supported constraints must be re-implemented to support the new type.

In this paper, we attempt to ease this second step. We describe a system for automatically deriving a native-code implementation of a global constraint (over novel variable types) from a declarative specification, complete with the ability to explain its propagation, a requirement if we want to make use of modern lazy clause generation CP solvers.

We demonstrate this approach by adding support for wrapped-integer variables to chuffed, a lazy clause generation CP solver.

Cite As Get BibTex

Graeme Gange and Peter J. Stuckey. Constraint Propagation and Explanation over Novel Types by Abstract Compilation. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/OASIcs.ICLP.2016.13

Author Details

Graeme Gange
Peter J. Stuckey

References

  1. Sébastien Bardin, Philippe Herrmann, and Florian Perroud. An Alternative to SAT-Based Approaches for Bit-Vectors. In Tools and Algorithms for the Construction and Analysis of Systems, number 6015 in LNCS, pages 84-98. Springer Berlin Heidelberg, March 2010. Google Scholar
  2. Ralph Becket. Specification of FlatZinc. [Online, accessed 3 March 2015], 2012. URL: http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf.
  3. N. Beldiceanu, M. Carlsson, and T. Petit. Deriving filtering algorithms from constraint checkers. In CP 2014, volume 3258, pages 107-122, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30201-8_11.
  4. Sebastian Brand and Roland H. C. Yap. Towards `propagation = logic + control'. In ICLP 2006, volume 4079, pages 102-116, 2006. URL: http://dx.doi.org/10.1007/11799573_10.
  5. Rafael Caballero, Peter J. Stuckey, and Antonio Tenorio-Fornes. Two type extensions for the constraint modelling language MiniZinc. Science of Computer Programming, 111:156-189, 2016. Google Scholar
  6. Geoffrey Chu. Improving Combinatorial Optimization. PhD thesis, Department of Computing and Information Systems, University of Melbourne, 2011. Google Scholar
  7. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL'77, pages 238-252, New York, NY, USA, 1977. URL: http://dx.doi.org/10.1145/512950.512973.
  8. Patrick Cousot and Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In PLILP'92, volume 631, pages 269-295, 1992. Google Scholar
  9. Patrick Cousot, Radhia Cousot, and Francesco Logozzo. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In VMCAI 2011, number 6538 in LNCS, pages 150-168. Springer Berlin Heidelberg, January 2011. Google Scholar
  10. William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22:269-285, 9 1957. URL: http://dx.doi.org/10.2307/2963594.
  11. Tristan Denmat, Arnaud Gotlieb, and Mireille Ducassé. An abstract interpretation based combinator for modelling while loops in constraint programming. In CP 2013, volume 4741, pages 241-255, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74970-7_19.
  12. Ian P. Gent, Christopher Jefferson, Steve Linton, Ian Miguel, and Peter Nightingale. Generating custom propagators for arbitrary constraints. Artif. Intell., 211:1-33, 2014. URL: http://dx.doi.org/10.1016/j.artint.2014.03.001.
  13. Arnaud Gotlieb, Michel Leconte, and Bruno Marre. Constraint solving on modular integers. In ModRef Workshop, associated to CP'2010, September 2010. Google Scholar
  14. C. Lattner and V. Adve. LLVM: a compilation framework for lifelong program analysis transformation. In CGO 2004, pages 75-86, March 2004. URL: http://dx.doi.org/10.1109/CGO.2004.1281665.
  15. Christopher Mears, Andreas Schutt, Peter J. Stuckey, Guido Tack, Kim Marriott, and Mark Wallace. Modelling with option types in minizinc. In CPAIOR 2014, number 8451 in LNCS, pages 88-103. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-07046-9_7.
  16. Jean-Noël Monette, Pierre Flener, and Justin Pearson. Towards solver-independent propagators. In CP 2012, volume 7514, pages 544-560, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33558-7_40.
  17. O. Ohrimenko, P.J. Stuckey, and M. Codish. Propagation via lazy clause generation. Constraints, 14(3):357-391, 2009. Google Scholar
  18. Marie Pelleau, Antoine Miné, Charlotte Truchet, and Frédéric Benhamou. A Constraint Solver Based on Abstract Domains. In VMCAI 2013, number 7737 in LNCS, pages 434-454. Springer Berlin Heidelberg, January 2013. Google Scholar
  19. P. Van Hentenryck, Vijay Saraswat, and Yves Deville. Constraint processing in cc(FD). Technical report, Computer Science Department, Brown University, 1992. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact