Solving complex problems using model transformations: from set constraint modeling to SAT instance solving - Université d'Angers Accéder directement au contenu
Article Dans Une Revue Expert Systems with Applications Année : 2020

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

Résumé

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.
Fichier principal
Vignette du fichier
ESWA_2019___paperV6 (1).pdf (294.05 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02945710 , version 1 (14-10-2021)

Identifiants

Citer

Frédéric Lardeux, Éric Monfroy, Eduardo Rodriguez-Tello, Broderick Crawford, Ricardo Soto. Solving complex problems using model transformations: from set constraint modeling to SAT instance solving. Expert Systems with Applications, 2020, 149, pp.113243. ⟨10.1016/j.eswa.2020.113243⟩. ⟨hal-02945710⟩

Collections

UNIV-ANGERS LERIA
29 Consultations
231 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More