Solving Max-SAT as weighted CSP - INRAE - Institut national de recherche pour l’agriculture, l’alimentation et l’environnement Accéder directement au contenu
Communication Dans Un Congrès Année : 2003

Solving Max-SAT as weighted CSP

Résumé

For the last ten years, a significant amount of work in the constraint community has been devoted to the improvement of complete methods for solving soft constraints networks. We wanted to see how recent progress in the weighted CSP (WCSP) field could compete with other approaches in related fields. One of these fields is propositional logic and the well-known Max-SAT problem. In this paper, we show how Max-SAT can be encoded as a weighted constraint network, either directly or using a dual encoding. We then solve Max-SAT instances using state-of-the-art algorithms for weighted Max-CSP, dedicated Max-SAT solvers and the state-of-the-art MIP solver CPLEX. The results show that, despite a limited adaptation to CNF structure, WCSP-solver based methods are competitive with existing methods and can even outperform them, especially on the hardest, most over-constrained problems.

Dates et versions

hal-02763945 , version 1 (04-06-2020)

Identifiants

Citer

Simon de Givry, Javier Larrosa, Pedro Meseguer, Thomas Schiex. Solving Max-SAT as weighted CSP. 9th International Conference on Principles and Practice of Constraint Programming - CP2003, Sep 2003, Kinsale, Ireland. pp.14, ⟨10.1007/978-3-540-45193-8_25⟩. ⟨hal-02763945⟩
9 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More