Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

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

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.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-02945710
Contributeur : Eric Monfroy Connectez-vous pour contacter le contributeur
Soumis le : jeudi 14 octobre 2021 - 11:26:23
Dernière modification le : mercredi 3 novembre 2021 - 06:08:43

Fichier

ESWA_2019___paperV6 (1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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, Elsevier, 2020, 149, pp.113243. ⟨10.1016/j.eswa.2020.113243⟩. ⟨hal-02945710⟩

Partager

Métriques

Consultations de la notice

30

Téléchargements de fichiers

15