DocumentCode :
2922717
Title :
Computing Horn Strong Backdoor Sets Thanks to Local Search
Author :
Paris, Lionel ; Ostrowski, Richard ; Siegel, Pierre ; Sais, Lakhdar
Author_Institution :
LSIS, Univ. de Provence, Marseille
fYear :
2006
fDate :
Nov. 2006
Firstpage :
139
Lastpage :
143
Abstract :
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 non-Horn 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
Keywords :
Boolean algebra; Horn clauses; computability; search problems; Boolean formula; Horn strong backdoor set; Horn subformula; Zchaff SAT solver; conjunctive normal form; local search; proportional satisfiability; Artificial intelligence; Data preprocessing; Formal verification; Large scale integration; Lenses; NP-complete problem; NP-hard problem; Polynomials; Space exploration; Stochastic systems;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Tools with Artificial Intelligence, 2006. ICTAI '06. 18th IEEE International Conference on
Conference_Location :
Arlington, VA
ISSN :
1082-3409
Print_ISBN :
0-7695-2728-0
Type :
conf
DOI :
10.1109/ICTAI.2006.43
Filename :
4031891
Link To Document :
بازگشت