Skip to main content
Log in

Satisfiability Testing for Boolean Formulas Using Δ-trees

Studia Logica Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. 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.

    Google Scholar 

  2. Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.

    Google Scholar 

  3. Claesen, L. J., editor. Formal VLSI correctness verification—VLSI design methods, volume 2. Elsevier, 1990.

  4. Gallier, J. H.. Logic for Computer Science: Foundations for Automatic Theorem Proving. Wiley & Sons, 1987.

  5. 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.

  6. 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.

  7. Murray, N. V., and E. Rosenthal. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504-535, 1993.

    Google Scholar 

  8. Paulson, L. C. Isabelle: a generic theorem prover. Lect. Notes in Comp. Sci. 828, 1994.

  9. Purdom, Jr., P. W. Average time for the full pure literal rule. Information Sciences, 78:269-291, 1994.

    Google Scholar 

  10. 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.

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints 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

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1020530109551

Navigation