Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Never Trust Your Solver: Certification for SAT and QBF

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2023)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 14101))

Included in the following conference series:

Abstract

Many problems for formal verification and artificial intelligence rely on advanced reasoning technologies in the background, often in the form of SAT or QBF solvers. Such solvers are sophisticated and highly tuned pieces of software, often too complex to be verified themselves. Now the question arises how one can one be sure that the result of such a solver is correct, especially when its result is critical for proving the correctness of another system. If a SAT solver, a tool for deciding a propositional formula, returns satisfiable, then it also returns a model which is easy to check. If the answer is unsatisfiable, the situation is more complicated. And so it is for true and false quantified Boolean formulas (QBFs), which extend propositional logic by quantifiers over the Boolean variables. To increase the trust in a solving result, modern solvers are expected to produce certificates that can independently and efficiently be checked. In this paper, we give an overview of the state of the art on validating the results of SAT and QBF solvers based on certification.

Supported by the LIT AI Lab Funded by the State of Upper Austria

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 74.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://satcompetition.github.io/2022/.

  2. 2.

    This example is inspired by an example presented in [10]

References

  1. Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39–55. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38916-0_3

    Chapter  Google Scholar 

  2. Ayari, A., Basin, D.: Qubos: deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X_12

    Chapter  Google Scholar 

  3. Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)

    Article  MATH  Google Scholar 

  4. Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_12

    Chapter  MATH  Google Scholar 

  5. Beyersdorff, O.: Proof complexity of quantified boolean logic-a survey. In: Mathematics for Computation (M4C), pp. 397–440. World Scientific (2023)

    Google Scholar 

  6. Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 81–93. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44465-8_8

    Chapter  MATH  Google Scholar 

  7. Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1–26:42 (2019)

    Google Scholar 

  8. Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd edn. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 1177–1221. IOS Press (2021)

    Google Scholar 

  9. Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005). https://doi.org/10.1007/11527695_5

    Chapter  MATH  Google Scholar 

  10. Biere, A.: SAT. Tutorial at the 5th Indian SAT and SMT Winter School (2020)

    Google Scholar 

  11. Biere, A., Fleury, M.: Gimsatul, IsaSAT and Kissat entering the SAT competition 2022. In: Balyo, T., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Procedings of SAT Competition 2022 - Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, vol. B-2022-1, pp. 10–11. University of Helsinki (2022)

    Google Scholar 

  12. Bloem, R., Braud-Santoni, N., Hadzic, V., Egly, U., Lonsing, F., Seidl, M.: Two SAT solvers for solving quantified boolean formulas with an arbitrary number of quantifier alternations. Formal Methods Syst. Des. 57(2), 157–177 (2021)

    Article  MATH  Google Scholar 

  13. Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_6

    Chapter  MATH  Google Scholar 

  14. Bryant, R.E., Heule, M.J.H.: Dual proof generation for quantified boolean formulas with a BDD-based solver. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 433–449. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-79876-5_25

    Chapter  Google Scholar 

  15. Buss, S., Nordström, J.: Proof complexity and SAT solving. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd edn. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 233–350. IOS Press (2021)

    Google Scholar 

  16. Buss, S., Thapen, N.: DRAT proofs, propagation redundancy, and extended resolution. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 71–89. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_5

    Chapter  MATH  Google Scholar 

  17. Chew, L., Clymo, J.: The equivalences of refutational QRAT. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 100–116. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_7

    Chapter  MATH  Google Scholar 

  18. Chew, L., Heule, M.J.H.: Relating existing powerful proof systems for QBF. In: Meel, K.S., Strichman, O. (eds.) Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). LIPIcs, vol. 236, pp. 10:1–10:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

    Google Scholar 

  19. Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220–236. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_14

    Chapter  Google Scholar 

  20. Gelder, A.V.: Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. In: International Symposium on Artificial Intelligence and Mathematics, (AI &M 2002) (2002)

    Google Scholar 

  21. Gelder, A.V.: Verifying RUP proofs of propositional unsatisfiability. In: Proceedings of the International Symposium on Artificial Intelligence and Mathematics (ISAIM 2008) (2008)

    Google Scholar 

  22. Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647–663. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33558-7_47

    Chapter  MATH  Google Scholar 

  23. Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: Dechter, R., Kearns, M.J., Sutton, R.S. (eds.) Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence (AAAI/IAAI 2002), pp. 649–654. AAAI Press/The MIT Press (2002)

    Google Scholar 

  24. Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), pp. 10886–10891. IEEE Computer Society (2003)

    Google Scholar 

  25. Goultiaeva, A., Gelder, A.V., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Walsh, T. (ed.) Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2012), pp. 546–553. IJCAI/AAAI (2011)

    Google Scholar 

  26. Hadzic, V., Bloem, R., Shukla, A., Seidl, M.: FERPModels: a certification framework for expansion-based QBF solving. In: Proceedings of the 24th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2022), pp. 80–83 (2022)

    Google Scholar 

  27. Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127–168 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  28. Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345–359. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_24

    Chapter  Google Scholar 

  29. Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 91–106. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_7

    Chapter  Google Scholar 

  30. Heule, M.J.H.: Proofs of unsatisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd edn., Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 635–668. IOS Press (2021)

    Google Scholar 

  31. Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 41–58. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_3

    Chapter  Google Scholar 

  32. Heule, M.J.H., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70–79 (2017)

    Article  Google Scholar 

  33. Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97–125 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  34. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  35. Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 230–244. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_19

    Chapter  Google Scholar 

  36. Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus q-resolution. Theor. Comput. Sci. 577, 25–42 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  37. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_28

    Chapter  Google Scholar 

  38. Kauers, M., Seidl, M.: Short proofs for some symmetric quantified boolean formulas. Inf. Process. Lett. 140, 4–7 (2018)

    Article  MathSciNet  MATH  Google Scholar 

  39. Kauers, M., Seidl, M.: Symmetries of quantified boolean formulas. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 199–216. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_13

    Chapter  MATH  Google Scholar 

  40. Kiesl, B., Heule, M.J.H., Seidl, M.: A little blocked literal goes a long way. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 281–297. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_18

    Chapter  Google Scholar 

  41. Kiesl, B., Rebola-Pardo, A., Heule, M.J.H., Biere, A.: Simulating strong practical proof systems with extended resolution. J. Autom. Reason. 64(7), 1247–1267 (2020)

    Article  MathSciNet  MATH  Google Scholar 

  42. Kiesl, B., Seidl, M.: QRAT polynomially simulates \(\forall \text{-Exp+Res }\). In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 193–202. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_13

    Chapter  Google Scholar 

  43. Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12–18 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  44. Knuth, D.: Handbook of Satisfiability (Quote on Backcover) (2021)

    Google Scholar 

  45. Kullmann, O.: Fundaments of branching heuristics. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, 2nd edn. Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 351–390. IOS Press (2021)

    Google Scholar 

  46. Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513–532 (2020)

    Article  MathSciNet  MATH  Google Scholar 

  47. Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45616-3_12

    Chapter  MATH  Google Scholar 

  48. Lonsing, F., Biere, A.: Nenofex: expanding NNF for QBF solving. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 196–210. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79719-7_19

    Chapter  Google Scholar 

  49. Lonsing, F., Biere, A.: Integrating Dependency Schemes in Search-Based QBF Solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 158–171. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_14

    Chapter  Google Scholar 

  50. Lonsing, F., Seidl, M., Gelder, A.V.: The QBF gallery: behind the scenes. Artif. Intell. 237, 92–114 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  51. Manthey, N., Lindauer, M.: SpyBug: automated bug detection in the configuration space of SAT Solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 554–561. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_36

    Chapter  MATH  Google Scholar 

  52. Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430–435. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_33

    Chapter  Google Scholar 

  53. Peitl, T., Slivovsky, F., Szeider, S.: Polynomial-time validation of QCDCL certificates. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 253–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_16

    Chapter  MATH  Google Scholar 

  54. Peitl, T., Slivovsky, F., Szeider, S.: Long-distance q-resolution with dependency schemes. J. Autom. Reason. 63(1), 127–155 (2019)

    Article  MathSciNet  MATH  Google Scholar 

  55. Pulina, L., Seidl, M.: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17). Artif. Intell. 274, 224–248 (2019)

    Article  MathSciNet  MATH  Google Scholar 

  56. Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27–30 September 2015, pp. 136–143. IEEE (2015)

    Google Scholar 

  57. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  58. Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. J. Autom. Reason. 42(1), 77–97 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  59. Schlaipfer, M., Slivovsky, F., Weissenbacher, G., Zuleger, F.: Multi-linear strategy extraction for QBF expansion proofs via local soundness. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 429–446. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51825-7_30

    Chapter  Google Scholar 

  60. Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified boolean formulas. In: Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2019), pp. 78–84. IEEE (2019)

    Google Scholar 

  61. Shukla, A., Slivovsky, F., Szeider, S.: Short Q-resolution proofs with homomorphisms. In: Pulina, L., Seidl, M. (eds.) SAT 2020. LNCS, vol. 12178, pp. 412–428. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51825-7_29

    Chapter  Google Scholar 

  62. Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 1996), pp. 220–227. IEEE Computer Society/ACM (1996)

    Google Scholar 

  63. Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 475–494. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_25

    Chapter  Google Scholar 

  64. Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021–2035 (2015)

    Article  Google Scholar 

  65. Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Pileggi, L.T., Kuehlmann, A. (eds.) Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design (ICCAD 2002), pp. 442–449. ACM / IEEE Computer Society (2002)

    Google Scholar 

  66. Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46135-3_14

    Chapter  Google Scholar 

  67. Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: Proceedings of the 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), pp. 10880–10885. IEEE Computer Society (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Symbolic Artificial Intelligence, Johannes Kepler University, Linz, Austria

    Martina Seidl

Authors
  1. Martina Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martina Seidl .

Editor information

Editors and Affiliations

  1. ENSIIE, Evry, France

    Catherine Dubois

  2. University of Birmingham, Birmingham, UK

    Manfred Kerber

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Seidl, M. (2023). Never Trust Your Solver: Certification for SAT and QBF. In: Dubois, C., Kerber, M. (eds) Intelligent Computer Mathematics. CICM 2023. Lecture Notes in Computer Science(), vol 14101. Springer, Cham. https://doi.org/10.1007/978-3-031-42753-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-42753-4_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-42752-7

  • Online ISBN: 978-3-031-42753-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation