Abstract
The problem of finding a small unsatisfiable core of an unsatisfiable CNF formula is addressed. The proposed algorithm, Trimmer, iterates over each internal node d in the resolution graph that ‘consumes’ a large number of clauses M (i.e. a large number of original clauses are present in the unsat core only for proving d) and attempts to prove them without the M clauses. If this is possible, it transforms the resolution graph into a new graph that does not have the M clauses at its core. Trimmer can be integrated into a fixpoint framework similarly to Malik and Zhang’s fix-point algorithm (run_till_fix). We call this option trim_till_fix. Experimental evaluation on a large number of industrial CNF unsatisfiable formulas shows that trim_till_fix doubles, on average, the number of reduced clauses in comparison to run_till_fix. It is also better when used as a component in a bigger system that enforces short timeouts.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Amla, N., McMillan, K.: Automatic abstraction without counter examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)
Bruni, R.: Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl. Math. 130(2), 85–100 (2003)
Georgiadis, L., Werneck, R.F., Tarjan, R.E., Triantafyllis, S., August, D.I.: Finding dominators in practice. In: Albers, S., Radzik, T. (eds.) ESA 2004. LNCS, vol. 3221, pp. 677–688. Springer, Heidelberg (2004)
Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided underapproximation-widening for multi-process systems. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 122–131. ACM Press, New York (2005)
Gupta, A.: Learning Abstractions for Model Checking. PhD thesis, Carnegie Mellon University (to be published, 2006)
Huang, J.: Mup: A minimal unsatisfiability prover. In: Proc. of the 10th Asia and South Pacific Design Automation Conference (ASP-DAC), pp. 432–437 (2005)
Koifman, M.: An approach to extracting a small unsatisfiable core. M.sc. thesis, Technion - I.I.T., Israel, Haifa (to be published, 2006)
Kroening, D., Ouaknine, J., Seshia, S., Strichman, O.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)
Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst. 1(1), 121–141 (1979)
Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: Proceedings of the International Symposium on Theory and Applications of Satisfiability Testing, pp. 305–310 (2004)
Oh, Y., Mneimneh, M.N., Andraus, Z.S., Sakallah, K.A., Markov, I.L.: Amuse: a minimally-unsatisfiable subformula extractor. In: DAC 2004, pp. 518–523 (2004)
Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. J. Comput. Syst. Sci. 37(1), 2–13 (1988)
Prosser, R.: Applications of boolean matrices to the analysis of flow diagrams. In: Proceedings of the Eastern Joint Computer Conference, pp. 133–138 (1959)
Shtrichman, O.: Prunning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 58. Springer, Heidelberg (2001)
Stump, A., Barrett, C., Dill, D.: CVC: a cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 500. Springer, Heidelberg (2002)
Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formula. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gershman, R., Koifman, M., Strichman, O. (2006). Deriving Small Unsatisfiable Cores with Dominators. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_13
Download citation
DOI: https://doi.org/10.1007/11817963_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)