Representative Encodings to Translate Finite CSPs into SAT

Pedro Manuel Corrêa Calvente de Barahona, Steffen Hölldobler, Nguyen Van-Hau

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

7 Citations (Scopus)

Abstract

Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding. Compared to the sparse and order encodings, two widely used and efficient encodings, these representative encodings require a smaller number of variables and longer clauses to express complex CSP constraints. The paper shows that, concerning unit propagation, these encodings are incomparable. Nevertheless, the preliminary experimental results show that the new representative encodings are clearly competitive with the original sparse and order encodings, but further studies are needed to better understand the trading between fewer variables and longer clauses of the representative encodings.
Original languageEnglish
Title of host publicationLecture Notes in Computer Science
PublisherAssociation for Computing Machinery (ACM)
Pages251-267
Volume8451
ISBN (Electronic)978-3-319-07046-9
ISBN (Print)978-3-319-07045-2
DOIs
Publication statusPublished - Jan 2014
EventCPAIOR 2014 - 11th International Conference on Integration of AI and OR Techniques in Constraint Programming -
Duration: 1 Jan 2014 → …

Conference

ConferenceCPAIOR 2014 - 11th International Conference on Integration of AI and OR Techniques in Constraint Programming
Period1/01/14 → …

Fingerprint

Constraint satisfaction problems

Keywords

    Cite this

    Barahona, P. M. C. C. D., Hölldobler, S., & Van-Hau, N. (2014). Representative Encodings to Translate Finite CSPs into SAT. In Lecture Notes in Computer Science (Vol. 8451, pp. 251-267). Association for Computing Machinery (ACM). https://doi.org/10.1007/978-3-319-07046-9_18
    Barahona, Pedro Manuel Corrêa Calvente de ; Hölldobler, Steffen ; Van-Hau, Nguyen. / Representative Encodings to Translate Finite CSPs into SAT. Lecture Notes in Computer Science. Vol. 8451 Association for Computing Machinery (ACM), 2014. pp. 251-267
    @inproceedings{958004316f36410396cf1c10718180d9,
    title = "Representative Encodings to Translate Finite CSPs into SAT",
    abstract = "Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding. Compared to the sparse and order encodings, two widely used and efficient encodings, these representative encodings require a smaller number of variables and longer clauses to express complex CSP constraints. The paper shows that, concerning unit propagation, these encodings are incomparable. Nevertheless, the preliminary experimental results show that the new representative encodings are clearly competitive with the original sparse and order encodings, but further studies are needed to better understand the trading between fewer variables and longer clauses of the representative encodings.",
    keywords = "SAT encodings, Constraint Satisfaction Problems",
    author = "Barahona, {Pedro Manuel Corr{\^e}a Calvente de} and Steffen H{\"o}lldobler and Nguyen Van-Hau",
    year = "2014",
    month = "1",
    doi = "10.1007/978-3-319-07046-9_18",
    language = "English",
    isbn = "978-3-319-07045-2",
    volume = "8451",
    pages = "251--267",
    booktitle = "Lecture Notes in Computer Science",
    publisher = "Association for Computing Machinery (ACM)",
    address = "United States",

    }

    Barahona, PMCCD, Hölldobler, S & Van-Hau, N 2014, Representative Encodings to Translate Finite CSPs into SAT. in Lecture Notes in Computer Science. vol. 8451, Association for Computing Machinery (ACM), pp. 251-267, CPAIOR 2014 - 11th International Conference on Integration of AI and OR Techniques in Constraint Programming, 1/01/14. https://doi.org/10.1007/978-3-319-07046-9_18

    Representative Encodings to Translate Finite CSPs into SAT. / Barahona, Pedro Manuel Corrêa Calvente de; Hölldobler, Steffen; Van-Hau, Nguyen.

    Lecture Notes in Computer Science. Vol. 8451 Association for Computing Machinery (ACM), 2014. p. 251-267.

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

    TY - GEN

    T1 - Representative Encodings to Translate Finite CSPs into SAT

    AU - Barahona, Pedro Manuel Corrêa Calvente de

    AU - Hölldobler, Steffen

    AU - Van-Hau, Nguyen

    PY - 2014/1

    Y1 - 2014/1

    N2 - Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding. Compared to the sparse and order encodings, two widely used and efficient encodings, these representative encodings require a smaller number of variables and longer clauses to express complex CSP constraints. The paper shows that, concerning unit propagation, these encodings are incomparable. Nevertheless, the preliminary experimental results show that the new representative encodings are clearly competitive with the original sparse and order encodings, but further studies are needed to better understand the trading between fewer variables and longer clauses of the representative encodings.

    AB - Solving Constraint Satisfaction Problems (CSPs) by Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that should not only be effectively generated, but should also be efficiently processed by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, focussing on two specific encodings: the representative-sparse encoding, already proposed albeit not thoroughly tested, and a new representative-order encoding. Compared to the sparse and order encodings, two widely used and efficient encodings, these representative encodings require a smaller number of variables and longer clauses to express complex CSP constraints. The paper shows that, concerning unit propagation, these encodings are incomparable. Nevertheless, the preliminary experimental results show that the new representative encodings are clearly competitive with the original sparse and order encodings, but further studies are needed to better understand the trading between fewer variables and longer clauses of the representative encodings.

    KW - SAT encodings

    KW - Constraint Satisfaction Problems

    U2 - 10.1007/978-3-319-07046-9_18

    DO - 10.1007/978-3-319-07046-9_18

    M3 - Conference contribution

    SN - 978-3-319-07045-2

    VL - 8451

    SP - 251

    EP - 267

    BT - Lecture Notes in Computer Science

    PB - Association for Computing Machinery (ACM)

    ER -

    Barahona PMCCD, Hölldobler S, Van-Hau N. Representative Encodings to Translate Finite CSPs into SAT. In Lecture Notes in Computer Science. Vol. 8451. Association for Computing Machinery (ACM). 2014. p. 251-267 https://doi.org/10.1007/978-3-319-07046-9_18