Scalable formula decomposition for propositional satisfiability

Propositional satisfiability solving, or SAT, is an important reasoning task arising in numerous applications, such as circuit design, formal verification, planning, scheduling or probabilistic reasoning. The depth-first search DPLL procedure is in practice the most efficient complete algorithm to date. Previous studies have shown the theoretical and experimental advantages of decomposing propositional formulas to guide the ordering of variable instantiation in DPLL. However, in practice, the computation of a tree decomposition may require a considerable amount of time and space on large formulas; existing decomposition tools are unable to handle most currently challenging SAT instances because of their size. In this paper, we introduce a simple, fast and scalable method to quickly produce tree decompositions of large SAT problems. We show experimentally the efficiency of orderings derived from these decompositions on the solving of challenging benchmarks. Categories and Subject Descr...

• Type: Conference
• Year: 2010
• Where: C3S2E
• Authors: Anthony Monnet, Roger Villemaire
• Keywords: C3S2E 2010, Important Reasoning Task, Propositional Satisfiability, Software Engineering, Tree Decompositions