Name
Title | ||
|---|---|---|
New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.disopt.2006.10.012 | Discrete Optimization |
Keywords | Field | DocType |
dpll algorithm,computational evaluation,new family,proposed heuristics,conflict-based search frameworks,dpll search technique,dpll satisfiability solvers,different value,different behavior,new score,sat- isfiability,dpll sat solver,satisfiability,branching rules,benchmark series,sat solver | Mathematical optimization,Satisfiability,Boolean satisfiability problem,Algorithm,Heuristics,DPLL algorithm,Solver,Mathematics,Branching (version control) | Journal |
Volume | Issue | ISSN |
5 | 3 | Discrete Optimization |
Citations | PageRank | References |
1 | 0.36 | 17 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Renato Bruni | 1 | 127 | 15.79 |
| Andrea Santori | 2 | 4 | 0.76 |