Abstract
The tree-based data structure of Δ-tree for propositional formulas is introduced in an improved and optimised form. The Δ-trees allow a compact representation for 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.
Similar content being viewed by others
References
Aguilera, G., I. P. De GuzmÁn, M. Ojeda-Aciego, and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science 266(1/2):81-112, 2001.
Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.
Claesen, L. J., editor. Formal VLSI correctness verification—VLSI design methods, volume 2. Elsevier, 1990.
Gallier, J. H.. Logic for Computer Science: Foundations for Automatic Theorem Proving. Wiley & Sons, 1987.
GutiÉrrez, G., I. P. De GuzmÁn, J. MartÍnez, M. Ojeda-Aciego, and A. Valverde. Reduction theorems for Boolean formulas using Δ-trees. In Proc. of JELIA 2000, pages 179-192. Lect. Notes in Artif. Intelligence 1919, 2000.
Massacci, F. Simplification: a general constraint propagation technique for propositional and modal tableaux. In Proceedings of Tableaux'98. Lect. Notes in Artificial Intelligence 1397, pages 217-231, 1998.
Murray, N. V., and E. Rosenthal. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504-535, 1993.
Paulson, L. C. Isabelle: a generic theorem prover. Lect. Notes in Comp. Sci. 828, 1994.
Purdom, Jr., P. W. Average time for the full pure literal rule. Information Sciences, 78:269-291, 1994.
Yang, B., Y. A. Chen, R. E. Bryant, and D. R. O'Hallaron. Space-and time-efficient BDD construction via working set control. In Proceedings of Asian-Pacific Design Automation Conference ASPDAC '98, pages 423-432, 1998.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Gutiérrez, G., de Guzmán, I.P., Martínez, J. et al. Satisfiability Testing for Boolean Formulas Using Δ-trees. Studia Logica 72, 85–112 (2002). https://doi.org/10.1023/A:1020530109551
Issue Date:
DOI: https://doi.org/10.1023/A:1020530109551