×

Satisfiability testing for Boolean formulas using \(\Delta\)-trees. (English) Zbl 1017.03003

Summary: The tree-based data structure of \(\Delta\)-tree for propositional formulas is introduced in an improved and optimised form. The \(\Delta\)-trees allow a compact representation of negation normal forms as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. These reduction strategies are divided into two subsets (meaning- and satisfiability-preserving transformations) and can be used to decrease the size of a negation normal form \(A\) at (at most) quadratic cost. The reduction strategies are aimed at decreasing the number of required branchings and, therefore, these strategies allow to limit the size of the search space for the SAT problem.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68P05 Data structures
PDFBibTeX XMLCite
Full Text: DOI