Marijn Heule, Armin Biere,
"Blocked Clause Decomposition"
: Proc. 19th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, Serie Lecture Notes in Computer Science, Vol. 8312, Springer, Seite(n) 423-438, 12-2013
Blocked Clause Decomposition
Sprache des Titels:
Proc. 19th Intl. Conf. on Logic for Programming, Artificial Intelligence and Reasoning
We demonstrate that it is fairly easy to decompose any
propositional formula into two subsets such that both can be solved by
blocked clause elimination. Such a blocked clause decomposition is useful
to cheaply detect backbone variables and equivalent literals. Blocked
clause decompositions are especially useful when they are unbalanced,
i.e., one subset is much larger in size than the other one. We present
algorithms and heuristics to obtain unbalanced decompositions efficiently.
Our techniques have been implemented in the state-of-the-art solver Lingeling.
Experiments show that the performance of Lingeling is clearly
improved due to these techniques on application benchmarks of the SAT