Document Open Access Logo

Long-Distance Q(D^std)-Consensus Is Sound

Authors Abhimanyu Choudhury , Meena Mahajan , Friedrich Slivovsky

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.12.pdf
  • Filesize: 0.75 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Quantified Boolean Formulas
  • Proof systems
  • Long-Distance Term Resolution / Consensus
  • Dependency Schemes

Metrics

Abstract

We describe a procedure that extracts existential strategies from verification proofs in the Long-Distance Consensus (i.e., Term Resolution) proof system when augmented with dependency schemes. We prove that when the standard dependency scheme 𝙳^std is used, the extracted strategies are winning strategies, thus establishing soundness of the proof system LDQ(D^std)-Consensus. We show through a counterexample that this approach fails to show soundness for LDQ(D^rrs)-Consensus.

Cite As Get BibTex

Abhimanyu Choudhury, Meena Mahajan, and Friedrich Slivovsky. Long-Distance Q(D^std)-Consensus Is Sound. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 12:1-12:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.12

Author Details

Abhimanyu Choudhury
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India
Meena Mahajan
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India
Friedrich Slivovsky
  • School of Computer Science & Informatics, University of Liverpool, UK

Funding

  • Mahajan, Meena: Supported in part from the ANRF J C Bose fellowship JCB/2023/000006.

References

  1. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 2012. URL: https://doi.org/10.1007/S10703-012-0152-6.
  2. Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, and Magdalena Widl. Efficient extraction of QBF (counter)models from long-distance resolution proofs. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, pages 3694-3701, 2015. URL: https://doi.org/10.1609/aaai.v29i1.9750.
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 154-169. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_12.
  4. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. J. Satisf. Boolean Model. Comput., 5(1-4):133-191, 2008. URL: https://doi.org/10.3233/SAT190055.
  5. Olaf Beyersdorff, Leroy Chew, and Mikolas Janota. On unification of QBF resolution-based calculi. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, volume 8635 of Lecture Notes in Computer Science, pages 81-93. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44465-8_8.
  6. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:7)2017.
  7. Armin Biere, Florian Lonsing, and Martina Seidl. Blocked clause elimination for QBF. In Nikolaj S. Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of Lecture Notes in Computer Science, pages 101-115. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_10.
  8. Joshua Blinkhorn and Olaf Beyersdorff. Shortening QBF proofs with dependency schemes. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 263-280. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_17.
  9. Roderick Bloem, Robert Könighofer, and Martina Seidl. SAT-based synthesis methods for safety specs. In Kenneth L. McMillan and Xavier Rival, editors, Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, volume 8318 of Lecture Notes in Computer Science, pages 1-20. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_1.
  10. Marco Cadoli, Marco Schaerf, Andrea Giovanardi, and Massimo Giovanardi. An algorithm to evaluate quantified boolean formulae and its experimental evaluation. J. Autom. Reason., 28(2):101-142, 2002. URL: https://doi.org/10.1023/A:1015019416843.
  11. Michael Cashmore, Maria Fox, and Enrico Giunchiglia. Partially grounded planning as quantified boolean formula. In Daniel Borrajo, Subbarao Kambhampati, Angelo Oddi, and Simone Fratini, editors, Proceedings of the Twenty-Third International Conference on Automated Planning and Scheduling, ICAPS 2013, Rome, Italy, June 10-14, 2013. AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS13/paper/view/5991.
  12. Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and Practice. Ph.d. thesis, Johannes Kepler University, Linz, Austria, 2012. Available online. URL: https://fmv.jku.at/papers/Lonsing-PhD-Thesis-2012.pdf.
  13. Florian Lonsing and Armin Biere. Integrating dependency schemes in search-based QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 158-171. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_14.
  14. Florian Lonsing and Armin Biere. DepQBF: A dependency-aware QBF solver. J. Satisf. Boolean Model. Comput., 7(2-3):71-76, 2010. URL: https://doi.org/10.3233/sat190077.
  15. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-resolution with dependency schemes. J. Autom. Reasoning, 63(1):127-155, 2019. URL: https://doi.org/10.1007/s10817-018-9467-3.
  16. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci., 612:83-101, 2016. URL: https://doi.org/10.1016/j.tcs.2015.10.020.
  17. Stefan Staber and Roderick Bloem. Fault localization and correction with QBF. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 355-368. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_34.
  18. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified boolean satisfiability solver. In Lawrence T. Pileggi and Andreas Kuehlmann, editors, Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, San Jose, California, USA, November 10-14, 2002, pages 442-449. ACM / IEEE Computer Society, 2002. URL: https://doi.org/10.1145/774572.774637.
  19. Lintao Zhang and Sharad Malik. The quest for efficient boolean satisfiability solvers. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 17-36. Springer, 2002. URL: https://doi.org/10.1007/3-540-45657-0_2.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact