Abstract
Robustness and correctness are essential criteria for SAT and QBF solvers. We develop automated testing and debugging techniques designed and optimized for SAT and QBF solver development. Our fuzz testing techniques are able to find critical solver defects that lead to crashes, invalid satisfying assignments and incorrect satisfiability results. Moreover, we show that sequential and concurrent delta debugging techniques are highly effective in minimizing failure-inducing inputs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Ansótegui, C., Béjar, R., Fernández, C., Mateu, C.: Generating Hard SAT/CSP Instances Using Expander Graphs. In: AAAI (2008)
Babić, D.: Exploiting Structure for Scalable Software Verification. PhD thesis, University of British Columbia, Vancouver, Canada (2008)
Benedetti, M.: sKizzo: A Suite to Evaluate and Certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 369–376. Springer, Heidelberg (2005)
Le Berre, D.: SAT4J: Bringing the Power of SAT Technology to the Java Platform, http://www.sat4j.org
Le Berre, D., Roussel, O., Simon, L.: SAT 2009 Competitive Events Booklet - Preliminary Version. In: SAT competition solver descriptions (September 2009), http://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf
Biere, A.: Resolve and Expand. In: SAT (Selected Papers) (2004)
Biere, A.: PicoSAT Essentials. JSAT 4 (2008)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)
Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: The Barcelogic SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294–298. Springer, Heidelberg (2008)
Bregman, D., Mitchell, D.: The SAT solver MXC, Version 0.5., SAT competition solver description (2007)
Brummayer, R., Biere, A.: Fuzzing and Delta-Debugging SMT Solvers. In: SMT. ACM International Conference Proceedings Series. ACM, New York (2009)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for Quantified Boolean Formulas. Inf. Comput. 117(1), 12–18 (1995)
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation. J. Autom. Reasoning 28 (2002)
Chen, H., Interian, Y.: A Model for Generating Random Quantified Boolean Formulas. In: IJCAI (2005)
Claessen, K., Hughes, J.: QuickCheck: a Lightweight Tool for Random Testing of Haskell Programs. ICFP 35(9) (2000)
Creignou, N., Daudé, H., Egly, U., Rossignol, R.: New Results on the Phase Transition for Random Quantified Boolean Formulas. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 34–47. Springer, Heidelberg (2008)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem-Proving. ACM Commun. 5 (1962)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, Depart. of Comp. and Inf. Science, University of Pennsylvania (1995)
Gebser, M., Kaufmann, B., Schaub, T.: The Conflict-Driven Answer Set Solver clasp: Progress Report. In: Erdem, E., Lin, F., Schaub, T. (eds.) LPNMR 2009. LNCS, vol. 5753, pp. 509–514. Springer, Heidelberg (2009)
Van Gelder, A.: Extracting (Easily) Checkable Proofs from a Satisfiability Solver that Employs both Preorder and Postorder Resolution. In: AMAI (2002)
Gent, I., Walsh, T.: The SAT Phase Transition. In: ECAI (1994)
Gent, I., Walsh, T.: Beyond NP: the QSAT phase transition. In: AAAI/IAAI (1999)
Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE++: An Efficient QBF Solver. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 201–213. Springer, Heidelberg (2004)
Hamadi, Y., Jabbour, S.: ManySAT: a Parallel SAT Solver. JSAT 6 (2009)
Heule, M.: SmArT Solving: Tools and Techniques for Satisfiability Solvers. PhD thesis, TU Delft (2008)
Horie, S., Watanabe, O.: Hard instance generation for SAT. CoRR, cs.CC/9809117 (1998)
Hsu, E., McIlraith, S.: VARSAT: Integrating Novel Probabilistic Interference Techniques with DPLL Search. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 377–390. Springer, Heidelberg (2009)
Huang, J.: TINISAT in SAT Competition 2007. SAT competition solver description (2007)
Jain, H., Clarke, E.: SAT Solver Descriptions: CMUSAT-Base and CMUSAT. SAT competition solver description (2007)
Jussila, T., Biere, A., Sinz, C., Kröning, D., Wintersteiger, C.: A First Step Towards a Unified Proof Checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 201–214. Springer, Heidelberg (2007)
Kern, C., Khaleghi, M., Kugele, S., Schallhart, C., Tautschnig, M., Weis, A.: SAT 7 - Engineering a Modular SAT-Solver. SAT competition solver description (2007)
Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, p. 160. Springer, Heidelberg (2002)
Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT Solving. In: Asia and South Pacific DAC (2007)
Lonsing, F.: DepQBF 0.1 Source Code (2010), http://fmv.jku.at/depqbf/
Miller, B., Koski, D., Lee, C., Maganty, V., Murthy, R., Natarajan, A., Steidl, J.: Fuzz Revisited: A Re-examination of the Reliability of UNIX Utilities and Services. Technical Report CS-TR-1995-1268, University of Wisconsin, Madison (1995)
Misherghi, G., Su, Z.: HDD: Hierarchical Delta Debugging. In: ICSE, pp. 142–151. ACM, New York (2006)
Narizzano, M., Peschiera, C., Pulina, L., Tacchella, A.: Evaluating and Certifying QBFs: A Comparison of State-of-the-Art Tools. AI Commun. 22 (2009)
Pan, G., Vardi, M.: Symbolic Decision Procedures for QBF. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 453–467. Springer, Heidelberg (2004)
Pennock, D., Stout, Q.: Exploiting a Theory of Phase Transitions in Three-Satisfiability Problems. In: AAAI/IAAI, vol. 1 (1996)
Pipatsrisawat, K., Darwiche, A.: RSat 2.0: SAT Solver Description. Technical Report D–153, Automated Reasoning Group, CSD, UCLA (2007)
Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa (2006)
Samulowitz, H.: MiniQBF Solver (2010), http://miniqbf.spaces.live.com/
Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 578–592. Springer, Heidelberg (2005)
Sutton, M., Greene, A., Amini, P.: Fuzzing - Brute Force Vulnerability Discovery. Pearson Ed., London (2007)
Takanen, A., Demott, J., Miller, C.: Fuzzing for Software Security Testing and Quality Assurance. Artech House (2008)
Tseitin, G.: On the Complexity of Proofs in Propositional Logics. Automation of Reasoning: Classical Papers in Computational Logic 1967-1970 2 (1983)
Xu, K., Boussemart, F., Hemery, F., Lecoutre, C.: A Simple Model to Generate Hard Satisfiable Instances. CoRR, abs/cs/0509032 (2005)
Yu, Y., Malik, S.: Validating the Result of a Quantified Boolean Formula (QBF) Solver: Theory and Practice. In: Asia and South Pacific DAC (2005)
Zeller, A.: Why Programs Fail. A Guide to Systematic Debugging. Morgan Kaufmann, San Francisco (2005)
Zeller, A., Hildebrandt, R.: Simplifying and Isolating Failure-Inducing Input. IEEE Transactions on Software Engineering 28(2), 183–200 (2002)
Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: DATE 2003 (2003)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brummayer, R., Lonsing, F., Biere, A. (2010). Automated Testing and Debugging of SAT and QBF Solvers. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14185-0
Online ISBN: 978-3-642-14186-7
eBook Packages: Computer ScienceComputer Science (R0)