|
EPIA'03 - 11th Portuguese Conference on Artificial Intelligence
CLPS -- Workshop on Constraint and Logic Programming Systems
|
Session: December 6, 17:15-18:45, Room A |
Title: |
Heuristic-Based Backtracking for Propositional Satisfiability |
|
A. Bhalla, I. Lynce, J. T. de Sousa and J. Marques-Silva |
Abstract: |
In recent years backtrack search algorithms for Propositional
Satisfiability (SAT) have been the subject of dramatic improvements.
These improvements allowed SAT solvers to successfully solve instances
with thousands of variables and hundreds of thousands of clauses, and
also motivated the development of many new challenging problem
instances, many of which still too hard for the current generation of SAT
solvers. As a result, further improvements to SAT technology are
expected to have key consequences in solving hard real-world
instances. The objective of this paper is to propose heuristic
approaches to the backtrack step of backtrack search SAT solvers, with
the goal of increasing the ability of a SAT solver to search
different parts of the search space. The proposed heuristics
are inspired by the heuristics proposed in recent years
for the branching step of SAT solvers, namely VSIDS and some of its
improvements. Moreover, the completeness of the new algorithm is
guaranteed. The preliminary experimental results are promising, and
motivate the integration of heuristic backtracking in state-of-the-art
SAT solvers. |
Back to schedule. |