Abstract
We focus on incremental compilation-to-SAT procedures (iCTS), a promising way to push standard SAT-based approaches beyond their limits. We propose the first comprehensive framework that encompasses all the aspects of an incremental decision procedure, from the encoding to the incremental solver. We apply our guidelines to a real-world CTS approach (Bounded Model Checking) and show how to modify both the generation mechanism of a real BMC tool (NuSMV) and the solving engine of a public-domain SAT solver (SIM). Related approaches and experimental results are discussed as well.
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
Abdulla, P.A., Bjesse, P., Eén, N.: Symbolic Reachability Analysis Based on SAT-Solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 411–425. Springer, Heidelberg (2000)
Benedetti, M., Bernardini, S.: Incremental Compilation-to-SAT Procedures. Technical Report T03-12-13 Istituto per la Ricerca Scientifica e Tecnologica (2003), http://sra.itc.it/people/benedetti/TR031213.pdf
Benedetti, M., Cimatti, A.: Bounded Model Checking for Past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)
Bennaceur, H., Gouachi, I., Plateau, G.: An Incremental Branch-and-Bound Method for Satisfiability Problem. INFORMS Journal on Computing 10, 301–308 (1998)
Bernardini, S.: Structure and Satisfiability in Propositional Formulae. AI*IA Notizie 4 (2003)
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 359. Springer, Heidelberg (2002)
Crawford, J.M., Baker, A.D.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proc. of 12th AAAI 1994, pp. 1092–1097 (1994)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM 5, 394–397 (1962)
Boy de la Tour, T.: Minimizing the Number of Clauses by Renaming. In: Proc. of the 10th Conference on Automated Deduction, pp. 558–572 (1990)
Eén, N., Sörensson, N.: Temporal Induction by Incremental SAT Solving. In: Proc. of the First International Workshop on Bounded Model Checking (2003)
Fu, Z.: zChaff (2003), http://ee.princeton.edu/~chaff/zchaff.php
Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, p. 347. Springer, Heidelberg (2001)
Hooker, J.N.: Solving the Incremental Satisfiability Problem. Journal of Logic Programming 15, 177–186 (1993)
Kautz, H., Selman, B.: Planning as satisfiability. In: Proc. of ECAI 1992, pp. 359–363 (1992)
Kim, J., Whittemore, J., Silva, J.P.M., Sakallah, K.A.: On Applying Incremental Satisfiability to Delay Fault Problem. In: Proc. of DATE 2000, pp. 380–384 (2000)
Kim, J., Whittemore, J., Silva, J.P.M., Sakallah, K.A.: On Solving Stack-Based Incremental Satisfiability Problems. In: Proc. of the ICCD 2000, pp. 379–382 (2000)
Larrabee, T.: Test pattern generation using boolean satisfiability. IEEE Transaction on Computer-aided Design, 4–15 (1992)
Massacci, F., Marraro, L.: Logical Cryptanalysis as a SAT Problem. Journal of Automated Reasoning 24 (2000)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 38th DAC, pp. 530–535 (2001)
Plaisted, D.A., Greenbaum, S.: A Structure-preserving Clause Form Translation. Journal of Symbolic Computation 2, 293–304 (1986)
Shtrichman, O.: Tuning SAT checkers for Bounded Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000)
Shtrichman, O.: Pruning Techniques for the SAT-based Bounded Model Checking Problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58–70. Springer, Heidelberg (2001)
Whittemore, J., Kim, J., Sakallah, K.A.: SATIRE: A New Incremental Satisfiability Engine. In: Proc. of the 38th Conference on Design Automation, pp. 542–545 (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
Benedetti, M., Bernardini, S. (2005). Incremental Compilation-to-SAT Procedures. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_4
Download citation
DOI: https://doi.org/10.1007/11527695_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27829-0
Online ISBN: 978-3-540-31580-3
eBook Packages: Computer ScienceComputer Science (R0)