Solving the all-interval series problem: SAT vs CP

Van-Hau Nguyen, Thai Son Mai

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

3 Citations (Scopus)

Abstract

Although Boolean satisfiability (abbreviated as SAT) is a sub-field of constraint programming (CP), the former states and solves problems as a black-box approach, whereas the latter aims at being tunable and programmable. Although many researches bridging SAT and CP have been provided, surprisingly, only few researchers have compared the SAT and CP approaches on a particular problem. This paper studies how to solve the all-interval series problem through both approaches. We will show that by using a state-of-the-art SAT solver and an appropriate SAT encoding the SAT approach obtains a significantly higher performance over the CP approach. Furthermore, we also provide the state-of-the-art result for several all-interval series instances.
Original languageEnglish
Title of host publicationProceedings of the Fifth Symposium on Information and Communication Technology
Pages65-74
DOIs
Publication statusPublished - 2014
Externally publishedYes

Keywords

  • Boolean Satisfiability Problem
  • Constraint Programming
  • Symmetry Breaking
  • The All-Inteveral Series Problem

Cite this