| Publication | Date of Publication | Type |
|---|
| Automated mathematical discovery and verification: minimizing pentagons in the plane | 2024-12-04 | Paper |
| Certified knowledge compilation with application to verified model counting | 2024-11-26 | Paper |
| Effective auxiliary variables via structured reencoding | 2024-11-26 | Paper |
| Exponential separations using guarded extension variables | 2024-09-25 | Paper |
| Without loss of satisfaction | 2024-09-13 | Paper |
| The packing chromatic number of the infinite square grid is at least 14 | 2024-07-12 | Paper |
| Relating existing powerful proof systems for QBF | 2024-07-12 | Paper |
| Migrating solver state | 2024-07-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6123937 | 2024-04-08 | Paper |
| Clausal proofs for pseudo-Boolean reasoning | 2024-01-23 | Paper |
| Moving definition variables in quantified Boolean formulas | 2024-01-23 | Paper |
| Propositional proof skeletons | 2023-12-13 | Paper |
| Unsatisfiability proofs for distributed clause-sharing SAT solvers | 2023-12-13 | Paper |
| The packing chromatic number of the infinite square grid is 15 | 2023-12-13 | Paper |
| Encoding Redundancy for Satisfaction-Driven Clause Learning | 2023-11-24 | Paper |
| Generating Extended Resolution Proofs with a BDD-Based SAT Solver | 2023-11-03 | Paper |
| Preprocessing of propagation redundant clauses | 2023-10-24 | Paper |
| An automated approach to the Collatz conjecture | 2023-06-27 | Paper |
| An Impossible Asylum | 2023-05-11 | Paper |
| SAT-Inspired Eliminations for Superposition | 2023-02-07 | Paper |
| The Packing Chromatic Number of the Infinite Square Grid is 15 | 2023-01-23 | Paper |
| A family of schemes for multiplying 3 × 3 matrices with 23 coefficient multiplications | 2023-01-11 | Paper |
| Preprocessing of propagation redundant clauses | 2022-12-07 | Paper |
| The resolution of Keller's conjecture | 2022-11-09 | Paper |
| The resolution of Keller's conjecture | 2022-10-24 | Paper |
| Tighter bounds on directed Ramsey number \(R(7)\) | 2022-09-28 | Paper |
| Skolem Function Continuation for Quantified Boolean Formulas | 2022-07-01 | Paper |
| Chinese remainder encoding for Hamiltonian cycles | 2022-03-22 | Paper |
| XOR local search for Boolean Brent equations | 2022-03-22 | Paper |
| SAT competition 2020 | 2021-12-13 | Paper |
| Dual proof generation for quantified Boolean formulas with a BDD-based solver | 2021-12-01 | Paper |
| An automated approach to the Collatz conjecture | 2021-12-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5164115 | 2021-11-09 | Paper |
| \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML | 2021-10-18 | Paper |
| Generating extended resolution proofs with a BDD-based SAT solver | 2021-08-04 | Paper |
| Sorting parity encodings by reusing variables | 2021-04-07 | Paper |
| Mycielski graphs and PR proofs | 2021-04-07 | Paper |
| New ways to multiply \(3 \times 3\)-matrices | 2021-02-18 | Paper |
| Avoiding Monochromatic Rectangles Using Shift Patterns | 2020-12-23 | Paper |
| Simulating strong practical proof systems with extended resolution | 2020-11-02 | Paper |
| Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions | 2020-08-05 | Paper |
| Truth Assignments as Conditional Autarkies | 2020-07-20 | Paper |
| Local search for fast matrix multiplication | 2020-05-20 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5219922 | 2020-03-09 | Paper |
| Strong extension-free proof systems | 2020-03-03 | Paper |
| The Implication Problem of Computing Policies | 2020-01-14 | Paper |
| Optimal symmetry breaking for graph problems | 2019-11-27 | Paper |
| The Resolution of Keller's Conjecture | 2019-10-08 | Paper |
| What a difference a variable makes | 2019-09-16 | Paper |
| Computing properties of stable configurations of thermodynamic binding networks | 2019-07-31 | Paper |
| Trimming Graphs Using Clausal Proof Optimization | 2019-07-01 | Paper |
| Computing Small Unit-Distance Graphs with Chromatic Number 5 | 2018-11-23 | Paper |
| Extended resolution simulates \({\mathsf{DRAT}}\) | 2018-10-18 | Paper |
| Efficient, verified checking of propositional proofs | 2018-01-04 | Paper |
| A little blocked literal goes a long way | 2017-11-15 | Paper |
| Efficient certified RAT verification | 2017-09-22 | Paper |
| Short proofs without new variables | 2017-09-22 | Paper |
| Avoiding triples in arithmetic progression | 2017-09-20 | Paper |
| Solution validation and extraction for QBF preprocessing | 2017-07-10 | Paper |
| Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer | 2016-09-05 | Paper |
| Computing Maximum Unavoidable Subgraphs Using SAT Solvers | 2016-09-05 | Paper |
| Reusing the assignment trail in CDCL solvers | 2016-02-23 | Paper |
| Compositional Propositional Proofs | 2016-01-12 | Paper |
| Expressing Symmetry Breaking in DRAT Proofs | 2015-12-02 | Paper |
| A SAT Approach to Clique-Width | 2015-09-17 | Paper |
| Clause Elimination for SAT and QSAT | 2015-08-25 | Paper |
| DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs | 2014-09-26 | Paper |
| A Unified Proof System for QBF Preprocessing | 2014-09-26 | Paper |
| MUS Extraction Using Clausal Proofs | 2014-09-26 | Paper |
| Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) | 2014-09-26 | Paper |
| Symmetry in Gardens of Eden | 2014-08-14 | Paper |
| Blocked Clause Decomposition | 2014-01-17 | Paper |
| Mechanical Verification of SAT Refutations with Extended Resolution | 2013-08-07 | Paper |
| A SAT Approach to Clique-Width | 2013-08-05 | Paper |
| Simulating circuit-level simplifications on CNF | 2013-07-05 | Paper |
| Verifying Refutations with Extended Resolution | 2013-06-14 | Paper |
| Revisiting Hyper Binary Resolution | 2013-06-04 | Paper |
| Inprocessing Rules | 2012-09-05 | Paper |
| Efficient CNF Simplification Based on Binary Implication Graphs | 2011-06-17 | Paper |
| Clause Elimination Procedures for CNF Formulas | 2010-10-12 | Paper |
| Exact DFA Identification Using SAT Solvers | 2010-09-10 | Paper |
| Blocked Clause Elimination | 2010-04-27 | Paper |
| Dynamic Symmetry Breaking by Simulating Zykov Contraction | 2009-07-07 | Paper |
| Effective Incorporation of Double Look-Ahead Procedures | 2009-03-10 | Paper |
| From Idempotent Generalized Boolean Assignments to Multi-bit Search | 2009-03-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3604001 | 2009-02-24 | Paper |
| Whose side are you on? Finding solutions in a biased search-tree | 2009-02-24 | Paper |
| Sums of squares based approximation algorithms for MAX-SAT | 2008-09-10 | Paper |
| Solving games dependence of applicable solving procedures | 2007-07-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3429156 | 2007-03-30 | Paper |
| A new method to construct lower bounds for van der Waerden numbers | 2007-03-12 | Paper |
| Theory and Applications of Satisfiability Testing | 2005-12-16 | Paper |
| Theory and Applications of Satisfiability Testing | 2005-12-16 | Paper |
| Theory and Applications of Satisfiability Testing | 2005-12-15 | Paper |
| Happy Ending: An Empty Hexagon in Every Set of 30 Points | N/A | Paper |
| PackIt! Gamified Rectangle Packing | N/A | Paper |
