Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Sergei Ovcharov. OBDD(Join) Proofs Cannot Be Balanced. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 72:1-72:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{ovcharov:LIPIcs.MFCS.2023.72, author = {Ovcharov, Sergei}, title = {{OBDD(Join) Proofs Cannot Be Balanced}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {72:1--72:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.72}, URN = {urn:nbn:de:0030-drops-186065}, doi = {10.4230/LIPIcs.MFCS.2023.72}, annote = {Keywords: Proof complexity, OBDD, lower bounds, depth of proofs} }
Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59, author = {Itsykson, Dmitry and Riazanov, Artur}, title = {{Automating OBDD proofs is NP-hard}}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)}, pages = {59:1--59:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-256-3}, ISSN = {1868-8969}, year = {2022}, volume = {241}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.59}, URN = {urn:nbn:de:0030-drops-168575}, doi = {10.4230/LIPIcs.MFCS.2022.59}, annote = {Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Dmitry Itsykson, Artur Riazanov, and Petr Smirnov. Tight Bounds for Tseitin Formulas. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 6:1-6:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{itsykson_et_al:LIPIcs.SAT.2022.6, author = {Itsykson, Dmitry and Riazanov, Artur and Smirnov, Petr}, title = {{Tight Bounds for Tseitin Formulas}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {6:1--6:21}, 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.6}, URN = {urn:nbn:de:0030-drops-166805}, doi = {10.4230/LIPIcs.SAT.2022.6}, annote = {Keywords: Proof complexity, Tseitin formulas, treewidth, resolution, OBDD-based proof systems} }
Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)
Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 3:1-3:34, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{itsykson_et_al:LIPIcs.CCC.2021.3, author = {Itsykson, Dmitry and Riazanov, Artur}, title = {{Proof Complexity of Natural Formulas via Communication Arguments}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {3:1--3:34}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-193-1}, ISSN = {1868-8969}, year = {2021}, volume = {200}, editor = {Kabanets, Valentine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.3}, URN = {urn:nbn:de:0030-drops-142773}, doi = {10.4230/LIPIcs.CCC.2021.3}, annote = {Keywords: bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, tree-like proofs} }
Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)
Anastasia Sofronova and Dmitry Sokolov. Branching Programs with Bounded Repetitions and Flow Formulas. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 17:1-17:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{sofronova_et_al:LIPIcs.CCC.2021.17, author = {Sofronova, Anastasia and Sokolov, Dmitry}, title = {{Branching Programs with Bounded Repetitions and Flow Formulas}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {17:1--17:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-193-1}, ISSN = {1868-8969}, year = {2021}, volume = {200}, editor = {Kabanets, Valentine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.17}, URN = {urn:nbn:de:0030-drops-142915}, doi = {10.4230/LIPIcs.CCC.2021.17}, annote = {Keywords: proof complexity, branching programs, bounded repetitions, lower bounds} }
Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)
Yaroslav Alekseev. A Lower Bound for Polynomial Calculus with Extension Rule. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 21:1-21:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{alekseev:LIPIcs.CCC.2021.21, author = {Alekseev, Yaroslav}, title = {{A Lower Bound for Polynomial Calculus with Extension Rule}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {21:1--21:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-193-1}, ISSN = {1868-8969}, year = {2021}, volume = {200}, editor = {Kabanets, Valentine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.21}, URN = {urn:nbn:de:0030-drops-142959}, doi = {10.4230/LIPIcs.CCC.2021.21}, annote = {Keywords: proof complexity, algebraic proofs, polynomial calculus} }
Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)
Fedor Part and Iddo Tzameret. Resolution with Counting: Dag-Like Lower Bounds and Different Moduli. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 19:1-19:37, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{part_et_al:LIPIcs.ITCS.2020.19, author = {Part, Fedor and Tzameret, Iddo}, title = {{Resolution with Counting: Dag-Like Lower Bounds and Different Moduli}}, booktitle = {11th Innovations in Theoretical Computer Science Conference (ITCS 2020)}, pages = {19:1--19:37}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-134-4}, ISSN = {1868-8969}, year = {2020}, volume = {151}, editor = {Vidick, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.19}, URN = {urn:nbn:de:0030-drops-117041}, doi = {10.4230/LIPIcs.ITCS.2020.19}, annote = {Keywords: Proof complexity, concrete lower bounds, resolution, satisfiability, combinatorics} }
Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 49:1-49:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{galesi_et_al:LIPIcs.MFCS.2019.49, author = {Galesi, Nicola and Itsykson, Dmitry and Riazanov, Artur and Sofronova, Anastasia}, title = {{Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {49:1--49:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-117-7}, ISSN = {1868-8969}, year = {2019}, volume = {138}, editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.49}, URN = {urn:nbn:de:0030-drops-109932}, doi = {10.4230/LIPIcs.MFCS.2019.49}, annote = {Keywords: Tseitin formula, treewidth, AC0-Frege} }
Published in: LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018)
Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 16:1-16:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{buss_et_al:LIPIcs.CCC.2018.16, author = {Buss, Sam and Itsykson, Dmitry and Knop, Alexander and Sokolov, Dmitry}, title = {{Reordering Rule Makes OBDD Proof Systems Stronger}}, booktitle = {33rd Computational Complexity Conference (CCC 2018)}, pages = {16:1--16:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-069-9}, ISSN = {1868-8969}, year = {2018}, volume = {102}, editor = {Servedio, Rocco A.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.16}, URN = {urn:nbn:de:0030-drops-88720}, doi = {10.4230/LIPIcs.CCC.2018.16}, annote = {Keywords: Proof complexity, OBDD, Tseitin formulas, the Clique-Coloring principle, lifting theorems} }
Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)
Ludmila Glinskih and Dmitry Itsykson. Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 26:1-26:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{glinskih_et_al:LIPIcs.MFCS.2017.26, author = {Glinskih, Ludmila and Itsykson, Dmitry}, title = {{Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {26:1--26:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.26}, URN = {urn:nbn:de:0030-drops-80767}, doi = {10.4230/LIPIcs.MFCS.2017.26}, annote = {Keywords: Tseitin formula, read-once branching program, expander} }
Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)
Dmitry Itsykson, Alexander Knop, Andrey Romashchenko, and Dmitry Sokolov. On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 43:1-43:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{itsykson_et_al:LIPIcs.STACS.2017.43, author = {Itsykson, Dmitry and Knop, Alexander and Romashchenko, Andrey and Sokolov, Dmitry}, title = {{On OBDD-Based Algorithms and Proof Systems That Dynamically Change Order of Variables}}, booktitle = {34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)}, pages = {43:1--43:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-028-6}, ISSN = {1868-8969}, year = {2017}, volume = {66}, editor = {Vollmer, Heribert and Vall\'{e}e, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.43}, URN = {urn:nbn:de:0030-drops-69914}, doi = {10.4230/LIPIcs.STACS.2017.43}, annote = {Keywords: Proof complexity, OBDD, error-correcting codes, Tseitin formulas, expanders} }
Published in: LIPIcs, Volume 64, 27th International Symposium on Algorithms and Computation (ISAAC 2016)
Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Complexity of Distributions and Average-Case Hardness. In 27th International Symposium on Algorithms and Computation (ISAAC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 64, pp. 38:1-38:12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
@InProceedings{itsykson_et_al:LIPIcs.ISAAC.2016.38, author = {Itsykson, Dmitry and Knop, Alexander and Sokolov, Dmitry}, title = {{Complexity of Distributions and Average-Case Hardness}}, booktitle = {27th International Symposium on Algorithms and Computation (ISAAC 2016)}, pages = {38:1--38:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-026-2}, ISSN = {1868-8969}, year = {2016}, volume = {64}, editor = {Hong, Seok-Hee}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2016.38}, URN = {urn:nbn:de:0030-drops-68083}, doi = {10.4230/LIPIcs.ISAAC.2016.38}, annote = {Keywords: average-case complexity, hierarchy theorem, sampling distributions, diagonalization} }
Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)
Dmitry Itsykson, Alexander Okhotin, and Vsevolod Oparin. Computational and Proof Complexity of Partial String Avoidability. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 51:1-51:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
@InProceedings{itsykson_et_al:LIPIcs.MFCS.2016.51, author = {Itsykson, Dmitry and Okhotin, Alexander and Oparin, Vsevolod}, title = {{Computational and Proof Complexity of Partial String Avoidability}}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)}, pages = {51:1--51:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-016-3}, ISSN = {1868-8969}, year = {2016}, volume = {58}, editor = {Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.51}, URN = {urn:nbn:de:0030-drops-64637}, doi = {10.4230/LIPIcs.MFCS.2016.51}, annote = {Keywords: partial strings, partial words, avoidability, proof complexity, PSPACE-completeness} }
Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)
Edward A. Hirsch and Dmitry Itsykson. On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 453-464, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{hirsch_et_al:LIPIcs.STACS.2010.2475, author = {Hirsch, Edward A. and Itsykson, Dmitry}, title = {{On Optimal Heuristic Randomized Semidecision Procedures, with Application to Proof Complexity}}, booktitle = {27th International Symposium on Theoretical Aspects of Computer Science}, pages = {453--464}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-16-3}, ISSN = {1868-8969}, year = {2010}, volume = {5}, editor = {Marion, Jean-Yves and Schwentick, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2475}, URN = {urn:nbn:de:0030-drops-24753}, doi = {10.4230/LIPIcs.STACS.2010.2475}, annote = {Keywords: Propositional proof complexity, optimal algorithm} }
Feedback for Dagstuhl Publishing