Solving complex problems using model transformations: from set constraint modeling to SAT instance solving

Frédéric Lardeux, Éric Monfroy, Eduardo Rodriguez-Tello, BRODERICK CRAWFORD LABRIN, RICARDO JAVIER SOTO DE GIORGIS

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

On the one hand, solvers for the propositional satisfiability problem (SAT) can deal with huge instances composed of millions of variables and clauses. On the other hand, Constraint Satisfaction Problems (CSP) can model problems as constraints over a set of variables with non-empty domains. They require combinatorial search methods as well as heuristics to be solved in a reasonable time. In this article, we present a technique that benefits from both expressive CSP modeling and efficient SAT solving. We model problems as CSP set constraints. Then, a propagation algorithm reduces the domains of variables by removing values that cannot participate in any valid assignment. The reduced CSP set constraints are transformed into a set of suitable SAT instances. They may be simplified by a preprocessing method before applying a standard SAT solver for computing their solutions. The practical usefulness of this technique is illustrated with two well-known problems: a) the Social Golfer, and b) the Sports Tournament Scheduling. We obtained competitive results either compared with ad hoc solvers or with hand-written SAT instances. Compared with direct SAT modeling, the proposed technique offers higher expressiveness, is less error-prone, and is relatively simpler to apply. The automatically generated propositional satisfiability instances are rather small in terms of clauses and variables. Hence, applying the constraint propagation phase, even huge instances of our problems can be tackled and efficiently solved.

Original languageEnglish
Article number113243
JournalExpert Systems with Applications
Volume149
DOIs
StatePublished - 1 Jul 2020
Externally publishedYes

Keywords

  • Combinatorial problem
  • Constraint programming
  • Model transformations
  • SAT encoding
  • Set constraints

Fingerprint Dive into the research topics of 'Solving complex problems using model transformations: from set constraint modeling to SAT instance solving'. Together they form a unique fingerprint.

Cite this