Skip to main content
SpringerLink
Log in

Davis and Putnam Meet Henkin: Solving DQBF with Resolution

  • 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

Davis-Putnam resolution is one of the fundamental theoretical decision procedures for both propositional logic and quantified Boolean formulas.

Dependency quantified Boolean formulas (DQBF) are a generalisation of QBF in which dependencies of variables are listed explicitly rather than being implicit in the order of quantifiers. Since DQBFs can succinctly encode synthesis problems that ask for Boolean functions matching a given specification, efficient DQBF solvers have a wide range of potential applications. We present a new decision procedure for DQBF in the style of Davis-Putnam resolution. Based on the merge resolution proof system, it directly constructs partial strategy functions for derived clauses. The procedure requires DQBF in a normal form called H-Form. We prove that the problem of evaluating DQBF in H-Form is NEXP-complete. In fact, we show that any DQBF can be converted into H-Form in linear time.

This research was supported by the Vienna Science and Technology Fund (WWTF) under grant number ICT19-060, and by the Austrian Science Fund (FWF) under grant number J-4361N.

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.

    The algorithm described by Davis and Putnam [12] also considers unit clauses and pure literals, but since these are neither necessary for completeness, nor complete on their own, we think of DP-resolution as consisting of variable elimination.

  2. 2.

    Note that we still take the if-then-else even if the functions are compatible, and in particular also if one of the functions is undefined. This is slightly counter-intuitive at first because we could just take the union in those cases, but the if-then-else results in a more compatible strategy and is in fact necessary to ensure completeness.

  3. 3.

    We cannot use soundness of \(\mathsf {M{\text{- }}Res}\), because our strategy compatibility notion is stronger.

  4. 4.

    In the size of the functions, which may, inevitably, become exponential.

References

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

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

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

  4. Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. J. Autom. Reasoning (2020). (in Press)

    Google Scholar 

  5. Giunchiglia, E., Tacchella, A. (eds.): SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004). https://doi.org/10.1007/b95238

    Book  Google Scholar 

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

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

  8. Buss, S.R., Hoffmann, J., Johannsen, J.: resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning. Logical Methods Comput. Sci. 4, (4), (2008). https://doi.org/10.2168/LMCS-4(4:13)2008, https://lmcs.episciences.org/860

  9. Buss, S.R., Kolodziejczyk, L.A.: Small stone in pool. Logical Methods Comput. Sci. 10(2), (2014). https://doi.org/10.2168/LMCS-10(2:16)2014, https://lmcs.episciences.org/852

  10. Cashmore, M., Fox, M., Long, D., Magazzeni, D.: A compilation of the full PDDL+ language into SMT. In: Coles, A.J., Coles, A., Edelkamp, S., Magazzeni, D., Sanner, S. (eds.) Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, ICAPS 2016, pp. 79–87. AAAI Press (2016)

    Google Scholar 

  11. Darwiche, A., Marquis, P.: A knowledge compilation map. J. Artif. Intell. Res. 17, 229–264 (2002) (electronic)

    Google Scholar 

  12. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)

    Article  MathSciNet  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. Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF, presented at Workshop on Pragmatics of SAT (POS) (2012). https://arise.or.at/pubpdf/Algorithm_for_Solving__DQBF_.pdf

  15. Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Berre, D.L. (ed.) Workshop on Pragmatics of SAT (POS). EPiC Series in Computing, vol. 27, pp. 103–116. EasyChair (2014)

    Google Scholar 

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

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  19. Meel, K.S., et al.: constrained sampling and counting: universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)

    Google Scholar 

  20. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symbolic Comput. 2(3), 293–304 (1986). https://doi.org/10.1016/S0747-7171(86)80028-1

    Article  MathSciNet  MATH  Google Scholar 

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

  22. Randal E. Bryant: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677–691 (1986). https://doi.org/10.1109/TC.1986.1676819

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

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

  25. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: Preliminary report. In: Aho, A.V., et al. (eds.) ACM Symposium on Theory of Computing (STOC), pp. 1–9. ACM (1973)

    Google Scholar 

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

  27. Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constructive Math. Math. Logic Part 2, 115–125 (1968)

    MATH  Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Friedrich-Schiller-Universität Jena, Jena, Germany

    Joshua Blinkhorn & Tomáš Peitl

  2. TU Wien, Vienna, Austria

    Friedrich Slivovsky

Authors
  1. Joshua Blinkhorn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tomáš Peitl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Friedrich Slivovsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tomáš Peitl .

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

Blinkhorn, J., Peitl, T., Slivovsky, F. (2021). Davis and Putnam Meet Henkin: Solving DQBF with Resolution. 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_4

Download citation

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

  • 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