Skip to main content
SpringerLink
Log in

Total Nondeterministic Turing Machines and a p-optimal Proof System for SAT

  • Conference paper
  • First Online:
Unveiling Dynamics and Complexity (CiE 2017)

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

Included in the following conference series:

  • 633 Accesses

Abstract

We show that the open problem of the existence of a p-optimal proof system for SAT can be characterized in terms of total nondeterministic Turing machines. We prove that there exists a p-optimal proof system for SAT if and only if there exists a proof system h for SAT such that for any total nondeterministic Turing machine working in polynomial time its totality is provable with short proofs in h and these proofs can be efficiently constructed. We prove that the standard proof system for SAT (a satisfying truth assignment is a proof of a satisfiable propositional formula) is p-optimal if and only if for any total nondeterministic Turing machine working in polynomial time its totality is provable with short proofs in the standard proof system for SAT and these proofs can be efficiently constructed.

Additionally we show that the problem of the existence of an optimal proof system for TAUT can be characterized in terms of pairs of nondeterministic Turing machines which are disjoint (do not accept the same strings). We prove that there exists an optimal proof system for TAUT if and only if there exists a proof system f for TAUT such that for any pair of disjoint nondeterministic Turing machines working in polynomial time their disjointness is provable in f with short proofs.

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. Balcazar, J., Díaz, J., Gabarró, J.: Structural Complexity I. Springer, Heidelberg (1995)

    Book  MATH  Google Scholar 

  2. Beyersdorff, O.: Classes of representable disjoint NP-pairs. Theoret. Comput. Sci. 377, 93–109 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  3. Beyersdorff, O.: Tuples of disjoint NP-sets. Theory Comput. Syst. 43(2), 118–135 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  4. Beyersdorff, O., Köbler, J., Messner, J.: Nondeterministic functions and the existence of optimal proof systems. Theoret. Comput. Sci. 410, 3839–3855 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  5. Beyersdorff, O., Sadowski, Z.: Do there exist complete sets for promise classes? Math. Logic Q. 57(6), 535–550 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  6. Cook, S.: The complexity of theorem proving procedures. In: Proceedings of the 3rd ACM Symposium on Theory of Computing, pp. 151–158 (1971)

    Google Scholar 

  7. Cook, S., Reckhow, R.: The relative efficiency of propositional proof systems. J. Symbolic Logic 44, 36–50 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  8. Fenner, S., Fortnow, L., Naik, A., Rogers, J.: Inverting onto functions. Inf. Comput. 186, 90–103 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  9. Köbler, J., Messner, J.: Complete problems for promise classes by optimal proof systems for test sets. In: Proceedings of the 13th IEEE Conference on Computational Complexity CCC 1998, pp. 132–140 (1998)

    Google Scholar 

  10. Köbler, J., Messner, J., Torán, J.: Optimal proof systems imply complete sets for promise classes. Inf. Comput. 184(1), 71–92 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  11. Krajíček, J., Pudlák, P.: Propositional proof systems, the consistency of first order theories and the complexity of computations. J. Symbolic Logic 54, 1063–1079 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  12. Messner, J.: On optimal algorithms and optimal proof systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 541–550. Springer, Heidelberg (1999). doi:10.1007/3-540-49116-3_51

    Chapter  Google Scholar 

  13. Pudlák, P.: Incompleteness in the finite domain. The Czech Academy of Science, Institute of Mathematics, Preprint No. 5–2016, Praha (2016)

    Google Scholar 

  14. Razborov, A.: On provably disjoint NP-pairs. Technical report 94–006, ECCC (1994)

    Google Scholar 

  15. Sadowski, Z.: On an optimal quantified propositional proof system and a complete language for NP \(\cap \) co-NP. In: Chlebus, B.S., Czaja, L. (eds.) FCT 1997. LNCS, vol. 1279, pp. 423–428. Springer, Heidelberg (1997). doi:10.1007/BFb0036203

    Chapter  Google Scholar 

Download references

Acknowledgements

I would like to thank the anonymous referees for all their helpful comments on how to improve the paper.

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Białystok, ul. Ciołkowskiego 1 M, 15-245, Białystok, Poland

    Zenon Sadowski

Authors
  1. Zenon Sadowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zenon Sadowski .

Editor information

Editors and Affiliations

  1. University of Turku, Turku, Finland

    Jarkko Kari

  2. Christian-Albrechts-University of Kiel, Kiel, Germany

    Florin Manea

  3. Åbo Akademi University, Turku, Finland

    Ion Petre

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Sadowski, Z. (2017). Total Nondeterministic Turing Machines and a p-optimal Proof System for SAT. In: Kari, J., Manea, F., Petre, I. (eds) Unveiling Dynamics and Complexity. CiE 2017. Lecture Notes in Computer Science(), vol 10307. Springer, Cham. https://doi.org/10.1007/978-3-319-58741-7_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-58741-7_34

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-58740-0

  • Online ISBN: 978-3-319-58741-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation