Gutiérrez, G.; de Guzmán, I. P.; Martínez, J.; Ojeda-Aciego, M.; Valverde, A. Satisfiability testing for Boolean formulas using \(\Delta\)-trees. (English) Zbl 1017.03003 Stud. Log. 72, No. 1, 85-112 (2002). 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. Cited in 2 Documents MSC: 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68P05 Data structures Keywords:data structures; automated deduction; propositional formulas; \(\Delta\)-trees; negation normal forms; satisfiability; reduction strategies; size of search space PDFBibTeX XMLCite \textit{G. Gutiérrez} et al., Stud. Log. 72, No. 1, 85--112 (2002; Zbl 1017.03003) Full Text: DOI