Skip to main content
SpringerLink
Log in

Proof Complexity of QBF Symmetry Recomputation

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

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

Abstract

For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs.

Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we propose a new formalism where symmetries are dynamically recomputed during the proof on restrictions of the original QBF. This presents a theoretical model for the potential use of symmetry recomputation as an inprocessing rule in QCDCL solving.

We demonstrate the power of symmetry recomputation by proving an exponential separation between Q-resolution with the symmetry rule and Q-resolution with our new symmetry recomputation rule. In fact, we show that bounding the number of symmetry recomputations gives rise to a hierarchy of QBF resolution systems of strictly increasing strength.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Dynamic symmetry-breaking for boolean satisfiability. Ann. Math. Artif. Intell. 57(1), 59–73 (2009)

    Article  MathSciNet  Google Scholar 

  2. Audemard, G., Jabbour, S., Sais, L.: Symmetry breaking in quantified boolean formulae. In: Veloso, M.M. (ed.) Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI 2007, pp. 2262–2267 (2007)

    Google Scholar 

  3. Audemard, G., Mazure, B., Sais, L.: Dealing with symmetries in quantified boolean formulas. In: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing (2004)

    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. Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319–351 (2004)

    Article  MathSciNet  Google Scholar 

  6. Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisfiability Boolean Model. Comput. 5(1–4), 133–191 (2008)

    MathSciNet  MATH  Google Scholar 

  7. Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost and capacity: a semantic technique for hard random QBFs. In: Karlin, A.R. (ed.) ACM Conference on Innovations in Theoretical Computer Science (ITCS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 94, pp. 9:1–9:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

    Google Scholar 

  8. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

    Google Scholar 

  9. Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. In: Lokam, S.V., Ramanujam, R. (eds.) Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs, vol. 93, pp. 14:1–14:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  10. Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 263–280. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_17

    Chapter  Google Scholar 

  11. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36–50 (1979)

    Article  MathSciNet  Google Scholar 

  12. Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104–122. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_8

    Chapter  MATH  Google Scholar 

  13. Devriendt, J., Bogaerts, B., Cat, B.D., Denecker, M., Mears, C.: Symmetry propagation: improved dynamic symmetry breaking in SAT. In: IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, pp. 49–56. IEEE Computer Society (2012)

    Google Scholar 

  14. Egly, U., Kronegger, M., Lonsing, F., Pfandler, A.: Conformant planning as a case study of incremental QBF solving. Ann. Math. Artif. Intell. 80(1), 21–45 (2017)

    Article  MathSciNet  Google Scholar 

  15. 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  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

  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. Krishnamurthy, B.: Short proofs for tricky formulas. Acta Inf. 22(3), 253–275 (1985)

    Article  MathSciNet  Google Scholar 

  20. Lonsing, F., Egly, U., Seidl, M.: Q-resolution with generalized axioms. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 435–452. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_27

    Chapter  Google Scholar 

  21. Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512–525 (2011)

    Article  MathSciNet  Google Scholar 

  22. Sakallah, K.A.: Symmetry and satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 289–338. IOS Press (2009)

    Google Scholar 

  23. Schaafsma, B., Heule, M.J.H., van Maaren, H.: Dynamic symmetry breaking by simulating Zykov contraction. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 223–236. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_22

    Chapter  Google Scholar 

  24. Szeider, S.: The complexity of resolution with generalized symmetry rules. Theory Comput. Syst. 38(2), 171–188 (2005)

    Article  MathSciNet  Google Scholar 

  25. Urquhart, A.: The symmetry rule in propositional logic. Discrete Appl. Math. 96–97, 177–193 (1999)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgments

Research was supported by grants from the John Templeton Foundation (grant no. 60842) and the Carl-Zeiss Foundation.

Author information

Authors and Affiliations

  1. Institut für Informatik, Friedrich-Schiller-Universität Jena, Jena, Germany

    Joshua Blinkhorn & Olaf Beyersdorff

Authors
  1. Joshua Blinkhorn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olaf Beyersdorff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Olaf Beyersdorff .

Editor information

Editors and Affiliations

  1. University of Lisbon, Lisbon, Portugal

    Mikoláš Janota

  2. University of Lisbon, Lisbon, Portugal

    Inês Lynce

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Blinkhorn, J., Beyersdorff, O. (2019). Proof Complexity of QBF Symmetry Recomputation. In: Janota, M., Lynce, I. (eds) Theory and Applications of Satisfiability Testing – SAT 2019. SAT 2019. Lecture Notes in Computer Science(), vol 11628. Springer, Cham. https://doi.org/10.1007/978-3-030-24258-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-24258-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-24257-2

  • Online ISBN: 978-3-030-24258-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation