Sciweavers

Share
DISOPT
2008

New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability

10 years 11 months ago
New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability
The paper is concerned with the computational evaluation and comparison of a new family of conflict-based branching heuristics for evolved DPLL Satisfiability solvers. Such a family of heuristics is based on the use of new scores updating criteria developed in order to overcome some of the typical unpleasant behaviors of DPLL search techniques. In particular, a score is associated with each literal. Whenever a conflict occurs, some scores are incremented with different values, depending on the character of the conflict. The branching variable is then selected by using the maximum among those scores. Several variants of this have been introduced into a state-of-the-art implementation of a DPLL SAT solver, obtaining several versions of the solver having quite different behavior. Experiments on many benchmark series, both satisfiable and unsatisfiable, demonstrate advantages of the proposed heuristics.
Renato Bruni, Andrea Santori
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where DISOPT
Authors Renato Bruni, Andrea Santori
Comments (0)
books