Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
A Hybrid Approach for SAT
| |
|
A Hybrid Approach for SAT
Djamal Habet5 , Chu Min Li6 , Laure Devendeville6 and Michel Vasquez5 
| (5) |
Centre LGI2P, éecole des Mines d’Alès, Site EERIE Parc Scientifique Georges Besse, 30035 Cedex 01, Nîes, France |
| (6) |
LaRIA, Université de Picardie Jules Verne, 5, Rue du Moulin Neuf, 80000 Amiens, France |
Abstract
Exploiting variable dependencies has been shown very useful in local search algorithms for SAT. In this paper, we extend the
use of such dependencies by hybridizing a local search algorithm, Walksat, and the DPLL procedure, Satz. At each node reached
in the DPLL search tree to a fixed depth, we construct the literal implication graph. Its strongly connected components are
viewed as equivalency classes. Each one is substituted by a unique representative literal to reduce the constructed graph
and the input formula. Finally, the implication dependencies are closed under transitivity. The resulted implications and
equivalencies are exploited by Walksat at each node of the DPLL tree. Our approach is motivated by the power of the branching
rule used in Satz that may provide a valid path to a solution, and generate more implications at deep nodes. Experimental
results confirm the efficiency of our approach.
This work is partially supported by French CNRS under grant number SUB/2001/0111/DR16
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|