Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann. Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{beyersdorff_et_al:LIPIcs.MFCS.2024.27, author = {Beyersdorff, Olaf and Hoffmann, Tim and Kasche, Kaspar and Spachmann, Luc Nicolas}, title = {{Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree}}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, pages = {27:1--27:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-335-5}, ISSN = {1868-8969}, year = {2024}, volume = {306}, editor = {Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.27}, URN = {urn:nbn:de:0030-drops-205834}, doi = {10.4230/LIPIcs.MFCS.2024.27}, annote = {Keywords: proof complexity, QBF, polynomial calculus, circuits, lower bounds} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Martina Seidl. Models and Counter-Models of Quantified Boolean Formulas (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{seidl:LIPIcs.SAT.2024.1, author = {Seidl, Martina}, title = {{Models and Counter-Models of Quantified Boolean Formulas}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {1:1--1:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.1}, URN = {urn:nbn:de:0030-drops-205238}, doi = {10.4230/LIPIcs.SAT.2024.1}, annote = {Keywords: Quantified Boolean Formula, Solution Extraction, Solution Counting} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2024.5, author = {Beyersdorff, Olaf and Fichte, Johannes K. and Hecher, Markus and Hoffmann, Tim and Kasche, Kaspar}, title = {{The Relative Strength of #SAT Proof Systems}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.5}, URN = {urn:nbn:de:0030-drops-205276}, doi = {10.4230/LIPIcs.SAT.2024.5}, annote = {Keywords: Model Counting, #SAT, Proof Complexity, Proof Systems, Lower Bounds, Knowledge Compilation} }
Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
Friedrich Slivovsky. Strategy Extraction by Interpolation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{slivovsky:LIPIcs.SAT.2024.28, author = {Slivovsky, Friedrich}, title = {{Strategy Extraction by Interpolation}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {28:1--28:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.28}, URN = {urn:nbn:de:0030-drops-205509}, doi = {10.4230/LIPIcs.SAT.2024.28}, annote = {Keywords: QBF, Expansion, Strategy Extraction, Interpolation} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12, author = {Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul}, title = {{From Proof Complexity to Circuit Complexity via Interactive Protocols}}, booktitle = {51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)}, pages = {12:1--12:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-322-5}, ISSN = {1868-8969}, year = {2024}, volume = {297}, editor = {Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12}, URN = {urn:nbn:de:0030-drops-201557}, doi = {10.4230/LIPIcs.ICALP.2024.12}, annote = {Keywords: proof complexity, circuit complexity, interactive protocols} }
Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)
Sravanthi Chede and Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{chede_et_al:LIPIcs.STACS.2023.21, author = {Chede, Sravanthi and Shukla, Anil}, title = {{Extending Merge Resolution to a Family of QBF-Proof Systems}}, booktitle = {40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)}, pages = {21:1--21:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-266-2}, ISSN = {1868-8969}, year = {2023}, volume = {254}, editor = {Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.21}, URN = {urn:nbn:de:0030-drops-176737}, doi = {10.4230/LIPIcs.STACS.2023.21}, annote = {Keywords: Proof complexity, QBFs, Merge Resolution, Simulation, Lower Bound} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Leroy Chew and Marijn J. H. Heule. Relating Existing Powerful Proof Systems for QBF. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{chew_et_al:LIPIcs.SAT.2022.10, author = {Chew, Leroy and Heule, Marijn J. H.}, title = {{Relating Existing Powerful Proof Systems for QBF}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {10:1--10:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-242-6}, ISSN = {1868-8969}, year = {2022}, volume = {236}, editor = {Meel, Kuldeep S. and Strichman, Ofer}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.10}, URN = {urn:nbn:de:0030-drops-166845}, doi = {10.4230/LIPIcs.SAT.2022.10}, annote = {Keywords: QBF, Proof Complexity, Verification, Strategy Extraction, Sequent Calculus} }
Published in: LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)
Leroy Chew and Friedrich Slivovsky. Towards Uniform Certification in QBF. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 22:1-22:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{chew_et_al:LIPIcs.STACS.2022.22, author = {Chew, Leroy and Slivovsky, Friedrich}, title = {{Towards Uniform Certification in QBF}}, booktitle = {39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)}, pages = {22:1--22:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-222-8}, ISSN = {1868-8969}, year = {2022}, volume = {219}, editor = {Berenbrink, Petra and Monmege, Benjamin}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.22}, URN = {urn:nbn:de:0030-drops-158326}, doi = {10.4230/LIPIcs.STACS.2022.22}, annote = {Keywords: QBF, Proof Complexity, Verification, Frege, Extended Frege, Strategy Extraction} }
Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2016.40, author = {Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil}, title = {{Understanding Cutting Planes for QBFs}}, booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)}, pages = {40:1--40:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-027-9}, ISSN = {1868-8969}, year = {2016}, volume = {65}, editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40}, URN = {urn:nbn:de:0030-drops-68758}, doi = {10.4230/LIPIcs.FSTTCS.2016.40}, annote = {Keywords: proof complexity, QBF, cutting planes, resolution, simulations} }
Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are Short Proofs Narrow? QBF Resolution is not Simple. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2016.15, author = {Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil}, title = {{Are Short Proofs Narrow? QBF Resolution is not Simple}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {15:1--15:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.15}, URN = {urn:nbn:de:0030-drops-57164}, doi = {10.4230/LIPIcs.STACS.2016.15}, annote = {Keywords: proof complexity, QBF, resolution, lower bound techniques, simulations} }
Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)
Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 76-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2015.76, author = {Beyersdorff, Olaf and Chew, Leroy and Janota, Mikol\'{a}s}, title = {{Proof Complexity of Resolution-based QBF Calculi}}, booktitle = {32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)}, pages = {76--89}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-78-1}, ISSN = {1868-8969}, year = {2015}, volume = {30}, editor = {Mayr, Ernst W. and Ollinger, Nicolas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.76}, URN = {urn:nbn:de:0030-drops-49057}, doi = {10.4230/LIPIcs.STACS.2015.76}, annote = {Keywords: proof complexity, QBF, lower bound techniques, separations} }
Feedback for Dagstuhl Publishing