Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2019: Theory and Applications of Satisfiability Testing – SAT 2019 pp 1–18Cite as

Circular (Yet Sound) Proofs

  • Conference paper
  • First Online:

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

Abstract

We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs circular. We show that, for all sets of standard inference rules, circular proofs are sound. We first focus on the circular version of Resolution, and see that it is stronger than Resolution since, as we show, the pigeonhole principle has circular Resolution proofs of polynomial size. Surprisingly, as proof systems for deriving clauses from clauses, Circular Resolution turns out to be equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find circular Resolution proofs of constant width, (2) examples that separate circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for circular Resolution. Contrary to the case of circular resolution, for Frege we show that circular proofs can be converted into tree-like ones with at most polynomial overhead.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. Atserias, A., Hakoniemi, T.: Size-degree trade-offs for sums-of-squares and Positivstellensatz proofs. To appear in Proceedings of 34th Annual Conference on Computational Complexity (CCC 2019) (2019). Long version in arXiv:1811.01351 [cs.CC] 2018

  2. Atserias, A., Lauria, M.: Circular (yet sound) proofs. CoRR, abs/1802.05266 (2018)

    Google Scholar 

  3. Atserias, A., Lauria, M., Nordström, J.: Narrow proofs may be maximally long. ACM Trans. Comput. Log. 17(3), 19:1–19:30 (2016)

    Article  MathSciNet  Google Scholar 

  4. Au, Y.H., Tunçel, L.: A comprehensive analysis of polyhedral lift-and-project methods. SIAM J. Discrete Math. 30(1), 411–451 (2016)

    Article  MathSciNet  Google Scholar 

  5. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. J. ACM 48(2), 149–169 (2001)

    Article  MathSciNet  Google Scholar 

  6. Bonet, M.L., Buss, S., Ignatiev, A., Marques-Silva, J., Morgado, A.: MaxSAT resolution with the dual rail encoding. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (2018)

    Google Scholar 

  7. Bonet, M.L., Esteban, J.L., Galesi, N., Johannsen, J.: On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput. 30(5), 1462–1484 (2000)

    Article  MathSciNet  Google Scholar 

  8. Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis, University of Edinburgh, November 2006

    Google Scholar 

  9. Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177–1216 (2011)

    Article  MathSciNet  Google Scholar 

  10. Buss, S.R.: Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Log. 52(4), 916–927 (1987)

    Article  MathSciNet  Google Scholar 

  11. Dantchev, S.S.: Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems. In: Proceedings of the 39th Annual ACM Symposium on Theory of Computing, pp. 311–317 (2007)

    Google Scholar 

  12. Dantchev, S.S., Martin, B., Rhodes, M.N.C.: Tight rank lower bounds for the Sherali-Adams proof system. Theor. Comput. Sci. 410(21–23), 2054–2063 (2009)

    Article  MathSciNet  Google Scholar 

  13. Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \({\mu }\)-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273–284. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_26

    Chapter  Google Scholar 

  14. Goerdt, A.: Cutting plane versus frege proof systems. In: Börger, E., Kleine Büning, H., Richter, M.M., Schönfeld, W. (eds.) CSL 1990. LNCS, vol. 533, pp. 174–194. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54487-9_59

    Chapter  Google Scholar 

  15. Grigoriev, D.: Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci. 259(1), 613–622 (2001)

    Article  MathSciNet  Google Scholar 

  16. Haken, A.: The intractability of resolution. Theor. Comp. Sci. 39, 297–308 (1985)

    Article  MathSciNet  Google Scholar 

  17. Ignatiev, A., Morgado, A., Marques-Silva, J.: On tackling the limits of resolution in SAT solving. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 164–183. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_11

    Chapter  MATH  Google Scholar 

  18. Krajíček, J.: Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge University Press, Cambridge (1994)

    MATH  Google Scholar 

  19. Niwiński, D., Walukiewicz, I.: Games for the \(\mu \)-calculus. Theor. Comp. Sci. 163(1), 99–116 (1996)

    Article  MathSciNet  Google Scholar 

  20. Pitassi, T., Segerlind, N.: Exponential lower bounds and integrality gaps for tree-like Lovász-Schrijver procedures. SIAM J. Comput. 41(1), 128–159 (2012)

    Article  MathSciNet  Google Scholar 

  21. Sherali, H.D., Adams, W.P.: A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Disc. Math. 3(3), 411–430 (1990)

    Article  MathSciNet  Google Scholar 

  22. Shoesmith, J., Smiley, T.J.: Multiple-Conclusion Logic. Cambridge University Press, Cambridge (1978)

    Book  Google Scholar 

  23. Studer, T.: On the proof theory of the modal mu-calculus. Studia Logica 89(3), 343–363 (2008)

    Article  MathSciNet  Google Scholar 

  24. Vinyals, M.: Personal communication (2018)

    Google Scholar 

Download references

Acknowledgments

Both authors were partially funded by European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement ERC-2014-CoG 648276 (AUTAR). First author partially funded by MICINN through TIN2016-76573-C2-1P (TASSAT3). We acknowledge the work of Jordi Coll who conducted experimental results for finding and visualizing actual circular resolution proofs of small instances of the sparse pigeonhole principle.

Author information

Authors and Affiliations

  1. Universitat Politècnica de Catalunya, Barcelona, Spain

    Albert Atserias

  2. Sapienza - Università di Roma, Rome, Italy

    Massimo Lauria

Authors
  1. Albert Atserias
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Massimo Lauria
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Massimo Lauria .

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

Atserias, A., Lauria, M. (2019). Circular (Yet Sound) Proofs. 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_1

Download citation

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

  • 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