Skip to main content
SpringerLink
Log in

Certified DQBF Solving by Definition Extraction

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2021 (SAT 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12831))

Abstract

We propose a new decision procedure for dependency quantified Boolean formulas (DQBFs) that uses interpolation-based definition extraction to compute Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop. In each iteration, a family of candidate Skolem functions is tested for correctness using a SAT solver, which either determines that a model has been found, or returns an assignment of the universal variables as a counterexample. Fixing a counterexample generally involves changing candidates of multiple existential variables with incomparable dependency sets. Our procedure introduces auxiliary variables—which we call arbiter variables—that each represent the value of an existential variable for a particular assignment of its dependency set. Possible repairs are expressed as clauses on these variables, and a SAT solver is invoked to find an assignment that deals with all previously seen counterexamples. Arbiter variables define the values of Skolem functions for assignments where they were previously undefined, and may lead to the detection of further Skolem functions by definition extraction.

A key feature of the proposed procedure is that it is certifying by design: for true DQBF, models can be returned at minimal overhead. Towards certification of false formulas, we prove that clauses can be derived in an expansion-based proof system for DQBF.

In an experimental evaluation on standard benchmark sets, a prototype implementation was able to match (and in some cases, surpass) the performance of state-of-the-art-solvers. Moreover, models could be extracted and validated for all true instances that were solved.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 89.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.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.

    An approach that does not fit this simplified classification is the First-Order solver iProver [29].

  2. 2.

    In these QBF solvers, Skolem functions are typically only indirectly represented by trees of formulas (abstractions) that encode viable assignments.

  3. 3.

    Available at https://github.com/perebor/pedant-solver.

  4. 4.

    The Penalized Average Runtime (PAR) is the average runtime, with the time for each unsolved instance calculated as a constant multiple of the timeout.

  5. 5.

    Due to the heavy-tailed runtime distribution of DQBF solvers, run-to-run variance rarely affects the number of solved instances. However, PAR2 scores should be taken with a grain of salt and only used to compare orders of magnitude.

  6. 6.

    With options –resolution 1 –univ_exp 0 –substitute 0.

References

  1. Akshay, S., Chakraborty, S., Goel, S., Kulal, S., Shah, S.: What’s hard about boolean functional synthesis? In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_14

    Chapter  Google Scholar 

  2. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp. 399–404 (2009)

    Google Scholar 

  3. Azhar, S., Peterson, G., Reif, J.: Lower bounds for multiplayer non-cooperative games of incomplete information. J. Comput. Math. Appl. 41, 957–992 (2001)

    Article  Google Scholar 

  4. Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86–100 (2014)

    Article  MathSciNet  Google Scholar 

  5. Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1–50:39 (2018)

    Google Scholar 

  6. Beyersdorff, O., Blinkhorn, J., Chew, L., Schmidt, R.A., Suda, M.: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. J. Autom. Reason. 63(3), 597–623 (2019)

    Article  MathSciNet  Google Scholar 

  7. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

  8. Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51–53. University of Helsinki (2020)

    Google Scholar 

  9. Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)

    Google Scholar 

  10. Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1–20. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_1

    Chapter  Google Scholar 

  11. Bubeck, U., Büning, H.K.: Dependency quantified horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 198–211. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_21

    Chapter  MATH  Google Scholar 

  12. 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). https://doi.org/10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  13. Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354–370. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_20

    Chapter  MATH  Google Scholar 

  14. Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 243–251. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_19

    Chapter  Google Scholar 

  15. Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF (2012). http://fmv.jku.at/papers/FroehlichKovasznaiBiere-POS12.pdf, presented at Workshop on Pragmatics of SAT (POS)

  16. Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: idq: instantiation-based DQBF solving. In: Berre, D.L. (ed.) POS-14. Fifth Pragmatics of SAT workshop, a workshop of the SAT 2014 conference, part of FLoC 2014 during the Vienna Summer of Logic,Vienna, Austria, 13 July 2014. EPiC Series in Computing, vol. 27, pp. 103–116. EasyChair (2014)

    Google Scholar 

  17. Ganian, R., Peitl, T., Slivovsky, F., Szeider, S.: Fixed-parameter tractability of dependency QBF with structural parameters. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, pp. 392–402 (2020)

    Google Scholar 

  18. Ge-Ernst, A., Scholl, C., Wimmer, R.: Localizing quantifiers for DQBF. In: Barrett, C.W., Yang, J. (eds.) Formal Methods in Computer Aided Design, FMCAD 2019, pp. 184–192. IEEE (2019)

    Google Scholar 

  19. Gitina, K., Reimer, S., Sauer, M., Wimmer, R., Scholl, C., Becker, B.: Equivalence checking of partial designs using dependency quantified boolean formulae. In: IEEE 31st International Conference on Computer Design, ICCD 2013, pp. 396–403. IEEE Computer Society (2013)

    Google Scholar 

  20. Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Nebel, W., Atienza, D. (eds.) Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, pp. 1617–1622. ACM (2015)

    Google Scholar 

  21. Golia, P., Roy, S., Meel, K.S.: Manthan: a data-driven approach for boolean function synthesis. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 611–633. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_31

    Chapter  Google Scholar 

  22. Gurfinkel, A., Vizel, Y.: Druping for interpolates. In: FMCAD 2014, pp. 99–106. IEEE (2014)

    Google Scholar 

  23. Heule, M.J.H., Järvisalo, M., Suda, M.: SAT competition 2018. J. Satisf. Boolean Model. Comput. 11(1), 133–154 (2019)

    MathSciNet  Google Scholar 

  24. Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: SAT, pp. 428–437 (2018)

    Google Scholar 

  25. Janota, M.: Towards generalization in QBF solving via machine learning. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), pp. 6607–6614. AAAI Press (2018)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  27. Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 67–82. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_7

    Chapter  MATH  Google Scholar 

  28. Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693–726 (2017)

    Article  MathSciNet  Google Scholar 

  29. Korovin, K.: iProver – an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_24

    Chapter  Google Scholar 

  30. Kullmann, O., Shukla, A.: Autarkies for DQCNF. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, pp. 179–183. IEEE (2019)

    Google Scholar 

  31. Meel, K.S., et al.: Constrained sampling and counting: Universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)

    Google Scholar 

  32. 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 

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

    Article  MathSciNet  Google Scholar 

  34. Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 314–325. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_20

    Chapter  Google Scholar 

  35. Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375–392. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_23

    Chapter  Google Scholar 

  36. Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisf. Boolean Model. Comput. 7(4), 139–144 (2011)

    MathSciNet  MATH  Google Scholar 

  37. Scholl, C., Becker, B.: Checking equivalence for partial implementations. In: Proceedings of the 38th Design Automation Conference, DAC 2001, pp. 238–243. ACM (2001)

    Google Scholar 

  38. Scholl, C., Jiang, J.R., Wimmer, R., Ge-Ernst, A.: A PSPACE subclass of dependency quantified boolean formulas and its effective solving. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, pp. 1584–1591. AAAI Press (2019)

    Google Scholar 

  39. Síč, J.: Satisfiability of DQBF using binary decision diagrams. Master’s thesis, Masaryk University, Brno, Czech Republic (2020)

    Google Scholar 

  40. Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 508–528. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_24

    Chapter  Google Scholar 

  41. Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83–101 (2016)

    Article  MathSciNet  Google Scholar 

  42. Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 136–148. ACM (2008)

    Google Scholar 

  43. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pp. 404–415. ACM (2006)

    Google Scholar 

  44. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24

    Chapter  Google Scholar 

  45. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., et al. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, Austin, Texas, USA, 30 April–2 May 1973, pp. 1–9. ACM (1973)

    Google Scholar 

  46. Tentrup, L.: CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput. 11(1), 155–210 (2019)

    MathSciNet  Google Scholar 

  47. Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 388–405. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_27

    Chapter  Google Scholar 

  48. Vizel, Y., Gurfinkel, A., Malik, S.: Fast interpolating BMC. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 641–657. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_43

    Chapter  Google Scholar 

  49. 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 

  50. Wimmer, R., Karrenbauer, A., Becker, R., Scholl, C., Becker, B.: From DQBF to QBF by dependency elimination. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 326–343. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_21

    Chapter  Google Scholar 

  51. Wimmer, R., Scholl, C., Becker, B.: The (D)QBF preprocessor hqspre - underlying theory and its implementation. J. Satisf. Boolean Model. Comput. 11(1), 3–52 (2019)

    MathSciNet  Google Scholar 

  52. Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 473–489. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_29

    Chapter  Google Scholar 

Download references

Acknowledgements

Supported by the Vienna Science and Technology Fund (WWTF) under the grants ICT19-060 and ICT19-065, and the Austrian Science Fund (FWF) under grant W1255.

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Franz-Xaver Reichl, Friedrich Slivovsky & Stefan Szeider

Authors
  1. Franz-Xaver Reichl
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Friedrich Slivovsky
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefan Szeider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Friedrich Slivovsky .

Editor information

Editors and Affiliations

  1. Laboratoire MIS, University of Picardie Jules Verne, Amiens, France

    Chu-Min Li

  2. IIIA-CSIC, Spanish National Research Council (CSIC), Bellaterra, Barcelona, Spain

    Felip Manyà

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Reichl, FX., Slivovsky, F., Szeider, S. (2021). Certified DQBF Solving by Definition Extraction. In: Li, CM., Manyà, F. (eds) Theory and Applications of Satisfiability Testing – SAT 2021. SAT 2021. Lecture Notes in Computer Science(), vol 12831. Springer, Cham. https://doi.org/10.1007/978-3-030-80223-3_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-80223-3_34

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-80222-6

  • Online ISBN: 978-3-030-80223-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation