| Publication | Date of Publication | Type |
|---|
| Experimental Repository for "Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability" | 2024-10-10 | Dataset |
| Certified CNF translations for pseudo-Boolean solving | 2024-07-12 | Paper |
| KRW composition theorems via lifting | 2024-05-22 | Paper |
| Certified Core-Guided MaxSAT Solving | 2024-04-26 | Paper |
| Certified dominance and symmetry breaking for combinatorial optimisation | 2023-10-23 | Paper |
| Experimental Repository for "Certified Core-Guided MaxSAT Solving" | 2023-05-25 | Dataset |
| Clique Is Hard on Average for Regular Resolution | 2022-12-08 | Paper |
| Nullstellensatz size-degree trade-offs from reversible pebbling | 2022-07-27 | Paper |
| Experimental Repository for "Certified CNF Translations for Pseudo-Boolean Solving" | 2022-06-06 | Dataset |
| Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search | 2022-02-10 | Paper |
| Nullstellensatz size-degree trade-offs from reversible pebbling | 2021-07-14 | Paper |
| Simplified and improved separations between regular and general resolution by lifting | 2021-04-07 | Paper |
| Experimental Repository for "Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning" | 2020-09-18 | Dataset |
| Using Resolution Proofs to Analyse CDCL SAT solvers | 2020-07-19 | Dataset |
| Composed Pebbling PHP pyramid instances in OPB format | 2020-07-14 | Dataset |
| Experimental Repository for "Learn to Relax: Integrating 0-1 Integer Linear Programming with Pseudo-Boolean Conflict-Driven Search" | 2020-07-13 | Dataset |
| https://portal.mardi4nfdi.de/entity/Q5111132 | 2020-05-26 | Paper |
| Supercritical Space-Width Trade-offs for Resolution | 2020-02-12 | Paper |
| Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs | 2019-12-01 | Paper |
| Clique is hard on average for regular resolution | 2019-08-22 | Paper |
| Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers | 2018-08-10 | Paper |
| In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving | 2018-08-10 | Paper |
| Cumulative Space in Black-White Pebbling and Resolution | 2018-05-03 | Paper |
| Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps | 2018-04-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4601842 | 2018-01-24 | Paper |
| A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds | 2018-01-24 | Paper |
| Supercritical Space-Width Trade-offs for Resolution | 2017-12-19 | Paper |
| Tight size-degree bounds for sums-of-squares proofs | 2017-12-18 | Paper |
| From Small Space to Small Width in Resolution | 2017-07-12 | Paper |
| Narrow Proofs May Be Maximally Long | 2017-07-12 | Paper |
| From small space to small width in resolution | 2017-03-03 | Paper |
| Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers | 2016-09-05 | Paper |
| On the Relative Strength of Pebbling and Resolution | 2015-09-17 | Paper |
| Space Complexity in Polynomial Calculus | 2015-09-02 | Paper |
| Narrow proofs may be spacious | 2014-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3191584 | 2014-10-06 | Paper |
| Long Proofs of (Seemingly) Simple Formulas | 2014-09-26 | Paper |
| A (Biased) Proof Complexity Survey for SAT Practitioners | 2014-09-26 | Paper |
| Some trade-off results for polynomial calculus | 2014-08-07 | Paper |
| On the virtue of succinct proofs | 2014-05-13 | Paper |
| Pebble games, proof complexity, and time-space trade-offs | 2013-09-26 | Paper |
| Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds | 2013-08-06 | Paper |
| On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution | 2011-07-06 | Paper |
| A simplified way of proving trade-off results for resolution | 2010-08-20 | Paper |
| Narrow Proofs May Be Spacious:Separating Space and Width in Resolution | 2010-03-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5302095 | 2009-01-05 | Paper |
| Certifying MIP-based Presolve Reductions for 0-1 Integer Linear Programs | N/A | Paper |
