Abstract
CNF Boolean formulas generated from resolution or solution enumeration often have much redundancy. Efficient algorithms are needed to simplify and compact such CNF formulas. In this paper, we present a novel algorithm to maintain a subsumption-free CNF clause database by efficiently detecting and removing subsumption as the clauses are being added. We then present an algorithm that compact CNF formula further by applying resolutions to make it Decremental Resolution Free. Our experimental evaluations show that these algorithms are efficient and effective in practice.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Tran. on Computers 48, 506–521 (1999)
Zhang, L., Malik, S.: Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, p. 200. Springer, Heidelberg (2002)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
Biere, A.: Resolve and Expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Subbarayan, S., Pradhan, D.K.: NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)
Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT Based Image Computation for Reachability Analysis. Technical Report CMU-CS-03-151, Carnegie Mellon University (July 2003)
de Kleer, J.: An Improved Incremental Algorithm for Generating Prime Implicates. In: Proc. of the 10th National Conference on Artificial Intelligence, AAAI 1992 (1992)
Chatalic, P., Simon, L.: Multi-Resolution on Compressed Sets of Clauses. In: Twelfth International Conference on Tools with Artificial Intelligence, ICTAI 2000 (2000)
Minato, S.: Zero-Suppressed BDDs for Set Manipula-tion in Combinatorial Problems. In: Proc. of the Design Automation Conference (DAC 1993), pp. 272–277 (1993)
Hachtel, G., Somenzi, F.: Logic Sysntheiss and Verification Algorithms. Kluwer Academic Publishers, Dordrecht (1996)
Kang, H.J., Park, I.-C.: SAT-Based Unbounded Symbolic Model Checking. In: Proc. 40th Design Automation Conference, DAC 2003 (2003)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Engineering an efficient SAT Solver. In: Proceedings of the Design Automation Conference (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, L. (2005). On Subsumption Removal and On-the-Fly CNF Simplification. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_42
Download citation
DOI: https://doi.org/10.1007/11499107_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)