Effective encodings of constraint programming models to SMT

Ewan Davidson, Ozgur Akgun, Joan Espasa Arxer, Peter Nightingale

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)
1 Downloads (Pure)

Abstract

Satisfiability Modulo Theories (SMT) is a well-established methodology that generalises propositional satisfiability (SAT) by adding support for a variety of theories such as integer arithmetic and bit-vector operations. SMT solvers have made rapid progress in recent years. In part, the efficiency of modern SMT solvers derives from the use of specialised decision procedures for each theory. In this paper we explore how the Essence Prime constraint modelling language can be translated to the standard SMT-LIB language. We target four theories: bit-vectors (QF_BV), linear integer arithmetic (QF_LIA), non-linear integer arithmetic (QF_NIA), and integer difference logic (QF_IDL). The encodings are implemented in the constraint modelling tool Savile Row. In an extensive set of experiments, we compare our encodings for the four theories, showing some notable differences and complementary strengths. We also compare our new encodings to the existing work targeting SMT and SAT, and to a well-established learning CP solver. Our two proposed encodings targeting the theory of bit-vectors (QF_BV) both substantially outperform earlier work on encoding to QF_BV on a large and diverse set of problem classes.
Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7–11, 2020, Proceedings
EditorsHelmut Simonis
PublisherSpringer
Pages143-159
ISBN (Electronic)9783030584757
ISBN (Print)9783030584740
DOIs
Publication statusPublished - 2020
Event26th International Conference on Principles and Practice of Constraint Programming (CP 2020) - Online, Louvain-la-Neuve, Belgium
Duration: 7 Sept 202011 Sept 2020
Conference number: 26
https://cp2020.a4cp.org/

Publication series

NameLecture Notes in Computer Science (Programming and Software Engineering)
PublisherSpringer
Volume12333 LNCS
ISSN (Print)0302-9743

Conference

Conference26th International Conference on Principles and Practice of Constraint Programming (CP 2020)
Abbreviated titleCP 2020
Country/TerritoryBelgium
CityLouvain-la-Neuve
Period7/09/2011/09/20
Internet address

Keywords

  • Constraint modelling
  • SMT
  • Automated reformulation

Fingerprint

Dive into the research topics of 'Effective encodings of constraint programming models to SMT'. Together they form a unique fingerprint.

Cite this