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 local search techniques finding assignment leading to largest renamable Horn sub-formula given CNF. More precisely, at each step, preference variables such that when assigned the opposite value lead smallest number remaining non- clauses. Consequently, if no positive or non clauses remain formula, our answer satisfiability formula; otherwise, non-Horn used extract set (Strong Backdoor) leads tractable sub-formula. Branching on significant improvements Zchaff SAT solver with respect many real worlds instances.