By the same authors

Effective Encodings of Constraint Programming Models to SMT

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

Full text download(s)

Author(s)

Department/unit(s)

Publication details

Title of host publicationProceedings of the 26th International Conference on Principles and Practice of Constraint Programming
DateAccepted/In press - 9 Jul 2020
DatePublished (current) - 7 Sep 2020
Pages143-159
Number of pages17
PublisherSpringer
Original languageEnglish
ISBN (Electronic)9783030584757
ISBN (Print)9783030584740

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12333
ISSN (Print)0302-9743

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.

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations