Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)
Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström. Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{mexi_et_al:LIPIcs.CP.2023.27, author = {Mexi, Gioni and Berthold, Timo and Gleixner, Ambros and Nordstr\"{o}m, Jakob}, title = {{Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning}}, booktitle = {29th International Conference on Principles and Practice of Constraint Programming (CP 2023)}, pages = {27:1--27:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-300-3}, ISSN = {1868-8969}, year = {2023}, volume = {280}, editor = {Yap, Roland H. C.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.27}, URN = {urn:nbn:de:0030-drops-190641}, doi = {10.4230/LIPIcs.CP.2023.27}, annote = {Keywords: Integer programming, pseudo-Boolean solving, conflict analysis, cutting planes proof system, mixed integer rounding, division, saturation} }
Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)
Talya Eden, Jakob Bæk Tejs Houen, Shyam Narayanan, Will Rosenbaum, and Jakub Tětek. Bias Reduction for Sum Estimation. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 62:1-62:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{eden_et_al:LIPIcs.APPROX/RANDOM.2023.62, author = {Eden, Talya and Houen, Jakob B{\ae}k Tejs and Narayanan, Shyam and Rosenbaum, Will and T\v{e}tek, Jakub}, title = {{Bias Reduction for Sum Estimation}}, booktitle = {Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)}, pages = {62:1--62:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-296-9}, ISSN = {1868-8969}, year = {2023}, volume = {275}, editor = {Megow, Nicole and Smith, Adam}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.62}, URN = {urn:nbn:de:0030-drops-188872}, doi = {10.4230/LIPIcs.APPROX/RANDOM.2023.62}, annote = {Keywords: bias reduction, sum estimation, sublinear time algorithms, sample complexity} }
Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)
Jakob Bæk Tejs Houen and Mikkel Thorup. A Sparse Johnson-Lindenstrauss Transform Using Fast Hashing. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 76:1-76:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{houen_et_al:LIPIcs.ICALP.2023.76, author = {Houen, Jakob B{\ae}k Tejs and Thorup, Mikkel}, title = {{A Sparse Johnson-Lindenstrauss Transform Using Fast Hashing}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {76:1--76:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.76}, URN = {urn:nbn:de:0030-drops-181281}, doi = {10.4230/LIPIcs.ICALP.2023.76}, annote = {Keywords: dimensionality reduction, hashing, concentration bounds, moment bounds} }
Published in: Dagstuhl Reports, Volume 12, Issue 10 (2023)
Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel. Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). In Dagstuhl Reports, Volume 12, Issue 10, pp. 84-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@Article{beyersdorff_et_al:DagRep.12.10.84, author = {Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy}, title = {{Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)}}, pages = {84--105}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2023}, volume = {12}, number = {10}, editor = {Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.10.84}, URN = {urn:nbn:de:0030-drops-178212}, doi = {10.4230/DagRep.12.10.84}, annote = {Keywords: Boolean satisfiability (SAT), SAT solving, computational complexity, proof complexity, combinatorial solving, combinatorial optimization, constraint programming, mixed integer linear programming} }
Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 16:1-16:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gocht_et_al:LIPIcs.SAT.2022.16, author = {Gocht, Stephan and Martins, Ruben and Nordstr\"{o}m, Jakob and Oertel, Andy}, title = {{Certified CNF Translations for Pseudo-Boolean Solving}}, booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}, pages = {16:1--16:25}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.16}, URN = {urn:nbn:de:0030-drops-166901}, doi = {10.4230/LIPIcs.SAT.2022.16}, annote = {Keywords: pseudo-Boolean solving, 0-1 integer linear program, proof logging, certifying algorithms, certified translation, CNF encoding, cutting planes} }
Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)
Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An Auditable Constraint Programming Solver. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{gocht_et_al:LIPIcs.CP.2022.25, author = {Gocht, Stephan and McCreesh, Ciaran and Nordstr\"{o}m, Jakob}, title = {{An Auditable Constraint Programming Solver}}, booktitle = {28th International Conference on Principles and Practice of Constraint Programming (CP 2022)}, pages = {25:1--25:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-240-2}, ISSN = {1868-8969}, year = {2022}, volume = {235}, editor = {Solnon, Christine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.25}, URN = {urn:nbn:de:0030-drops-166548}, doi = {10.4230/LIPIcs.CP.2022.25}, annote = {Keywords: Constraint programming, proof logging, auditable solving} }
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-dev.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)
Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The Power of Negative Reasoning. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{derezende_et_al:LIPIcs.CCC.2021.40, author = {de Rezende, Susanna F. and Lauria, Massimo and Nordstr\"{o}m, Jakob and Sokolov, Dmitry}, title = {{The Power of Negative Reasoning}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {40:1--40:24}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.40}, URN = {urn:nbn:de:0030-drops-143140}, doi = {10.4230/LIPIcs.CCC.2021.40}, annote = {Keywords: Proof complexity, Polynomial calculus, Nullstellensatz, Sums-of-squares, Sherali-Adams} }
Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)
Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 28:1-28:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{derezende_et_al:LIPIcs.CCC.2020.28, author = {de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Risse, Kilian and Sokolov, Dmitry}, title = {{Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs}}, booktitle = {35th Computational Complexity Conference (CCC 2020)}, pages = {28:1--28:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-156-6}, ISSN = {1868-8969}, year = {2020}, volume = {169}, editor = {Saraf, Shubhangi}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.28}, URN = {urn:nbn:de:0030-drops-125804}, doi = {10.4230/LIPIcs.CCC.2020.28}, annote = {Keywords: proof complexity, resolution, weak pigeonhole principle, perfect matching, sparse graphs} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Ambrus Kaposi and Jakob von Raumer. A Syntax for Mutual Inductive Families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{kaposi_et_al:LIPIcs.FSCD.2020.23, author = {Kaposi, Ambrus and von Raumer, Jakob}, title = {{A Syntax for Mutual Inductive Families}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {23:1--23:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.23}, URN = {urn:nbn:de:0030-drops-123451}, doi = {10.4230/LIPIcs.FSCD.2020.23}, annote = {Keywords: type theory, inductive types, mutual inductive types, W-types, Agda} }
Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)
Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky. Trade-Offs Between Size and Degree in Polynomial Calculus. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{lagarde_et_al:LIPIcs.ITCS.2020.72, author = {Lagarde, Guillaume and Nordstr\"{o}m, Jakob and Sokolov, Dmitry and Swernofsky, Joseph}, title = {{Trade-Offs Between Size and Degree in Polynomial Calculus}}, booktitle = {11th Innovations in Theoretical Computer Science Conference (ITCS 2020)}, pages = {72:1--72:16}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.72}, URN = {urn:nbn:de:0030-drops-117573}, doi = {10.4230/LIPIcs.ITCS.2020.72}, annote = {Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, size-degree trade-off, resolution, colored polynomial local search} }
Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)
Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{derezende_et_al:LIPIcs.CCC.2019.18, author = {de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Meir, Or and Robere, Robert}, title = {{Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling}}, booktitle = {34th Computational Complexity Conference (CCC 2019)}, pages = {18:1--18:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-116-0}, ISSN = {1868-8969}, year = {2019}, volume = {137}, editor = {Shpilka, Amir}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.18}, URN = {urn:nbn:de:0030-drops-108403}, doi = {10.4230/LIPIcs.CCC.2019.18}, annote = {Keywords: proof complexity, Nullstellensatz, pebble games, trade-offs, size, degree} }
Published in: Dagstuhl Reports, Volume 8, Issue 1 (2018)
Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam. Proof Complexity (Dagstuhl Seminar 18051). In Dagstuhl Reports, Volume 8, Issue 1, pp. 124-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@Article{atserias_et_al:DagRep.8.1.124, author = {Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul}, title = {{Proof Complexity (Dagstuhl Seminar 18051)}}, pages = {124--157}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2018}, volume = {8}, number = {1}, editor = {Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.8.1.124}, URN = {urn:nbn:de:0030-drops-92864}, doi = {10.4230/DagRep.8.1.124}, annote = {Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms} }
Published in: LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)
Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. Cumulative Space in Black-White Pebbling and Resolution. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{alwen_et_al:LIPIcs.ITCS.2017.38, author = {Alwen, Jo\"{e}l and de Rezende, Susanna F. and Nordstr\"{o}m, Jakob and Vinyals, Marc}, title = {{Cumulative Space in Black-White Pebbling and Resolution}}, booktitle = {8th Innovations in Theoretical Computer Science Conference (ITCS 2017)}, pages = {38:1--38:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-029-3}, ISSN = {1868-8969}, year = {2017}, volume = {67}, editor = {Papadimitriou, Christos H.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.38}, URN = {urn:nbn:de:0030-drops-81918}, doi = {10.4230/LIPIcs.ITCS.2017.38}, annote = {Keywords: pebble game, pebbling, proof complexity, space, cumulative space, clause space, resolution, parallel resolution} }
Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)
Massimo Lauria and Jakob Nordström. Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{lauria_et_al:LIPIcs.CCC.2017.2, author = {Lauria, Massimo and Nordstr\"{o}m, Jakob}, title = {{Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gr\"{o}bner Bases}}, booktitle = {32nd Computational Complexity Conference (CCC 2017)}, pages = {2:1--2:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-040-8}, ISSN = {1868-8969}, year = {2017}, volume = {79}, editor = {O'Donnell, Ryan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.2}, URN = {urn:nbn:de:0030-drops-75410}, doi = {10.4230/LIPIcs.CCC.2017.2}, annote = {Keywords: proof complexity, Nullstellensatz, Gr\"{o}bner basis, polynomial calculus, cutting planes, colouring} }
Feedback for Dagstuhl Publishing