Loading...
Please wait, while we are loading the content...
Similar Documents
A logical approach to efficient max-sat solving (2006).
| Content Provider | CiteSeerX |
|---|---|
| Author | Larrosa, Javier Heras, Federico Givry, Simon De |
| Abstract | 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 focus 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 expressable in logic terms with our framework in a unified manner. Besides, we 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, show |
| File Format | |
| Publisher Date | 2006-01-01 |
| Access Restriction | Open |
| Subject Keyword | Logical Approach Basic Sat Comprehensive Max-sat Evaluation Considerable Interest Many Important Problem Work Focus Weighted Max-sat Several Benchmark Logic Term Weighted Resolution Important Problem State-of-the-art Max-sat Solver Procedural Way Dpll-like Algorithm Many Algorithmic Trick Restricted Amount Unified Manner Original Search Algorithm Good Quality Original Framework Optimization Version Recent Year Classical Sat Practical Point Visited Node |
| Content Type | Text |
| Resource Type | Article |
