A logical approach to efficient Max-SAT solving

Weighted Max-SAT is the optimization version of SAT and many important problems can be naturally encoded as such. Solving weighted Max-SAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving...

Full description

Saved in:
Bibliographic Details
Published in:Artificial intelligence 2008-02, Vol.172 (2), p.204-233
Main Authors: Larrosa, Javier, Heras, Federico, de Givry, Simon
Format: Article
Language:English
Subjects:
Applied sciences
Artificial intelligence
Computer Science
Computer science
control theory
systems
Exact sciences and technology
Inference
Learning and adaptive systems
Mathematics
Max-SAT
Search
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Weighted Max-SAT is the optimization version of SAT and many important problems can be naturally encoded as such. Solving weighted Max-SAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving techniques. Most of this work focuses on the computation of good quality lower bounds to be used within a branch and bound DPLL-like algorithm. Most often, these lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce an original framework for Max-SAT that stresses the parallelism with classical SAT. Then, we extend the two basic SAT solving techniques: search and inference. We show that many algorithmic tricks used in state-of-the-art Max-SAT solvers are easily expressible in logical terms in a unified manner, using our framework. We also introduce an original search algorithm that performs a restricted amount of weighted resolution at each visited node. We empirically compare our algorithm with a variety of solving alternatives on several benchmarks. Our experiments, which constitute to the best of our knowledge the most comprehensive Max-SAT evaluation ever reported, demonstrate the practical usability of our approach.
ISSN:0004-3702
1872-7921
DOI:10.1016/j.artint.2007.05.006