Decomposing Boolean Formulas into Connected Components
Tomáš Balyo · 2011
The aim of this contribution is to find a way how to improve eciency of current state-of-the-art satisfiability solvers. The idea is to split a given instance of the problem into parts (connected components) which can be solved separately. For this purpose we define component trees and a related problem of finding optimal component trees. We describe how this approach can be combined with standard satisfiability solver decision heuristics to improve them. The proposed ideas were implemented and experimentally evaluated on a large set of benchmark problems. We provide results of these experiments.