Sciweavers

Share
ICTAI
2006
IEEE

Computing Horn Strong Backdoor Sets Thanks to Local Search

10 years 7 months ago
Computing Horn Strong Backdoor Sets Thanks to Local Search
In this paper a new approach for computing Strong Backdoor sets of boolean formula in conjunctive normal form (CNF) is proposed. It makes an original use of local search techniques for finding an assignment leading to a largest renamable Horn sub-formula of a given CNF. More precisely, at each step, preference is given to variables such that when assigned to the opposite value lead to the smallest number of remaining nonHorn clauses. Consequently, if no positive or non Horn clauses remain in the formula, our approach answer the satisfiability of the original formula; otherwise, a smallest non-Horn sub-formula is used to extract the set of variables (Strong Backdoor) such that when assigned leads to a tractable sub-formula. Branching on the variables of the Strong Backdoor set leads to significant improvements of Zchaff SAT solver with respect to many real worlds SAT instances.
Lionel Paris, Richard Ostrowski, Pierre Siegel, La
Added 11 Jun 2010
Updated 11 Jun 2010
Type Conference
Year 2006
Where ICTAI
Authors Lionel Paris, Richard Ostrowski, Pierre Siegel, Lakhdar Sais
Comments (0)
books