| 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 |
| Easier variants of notorious math problems | 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
Tools and Algorithms for the Construction and Analysis of Systems | 2023-11-24 | Paper |
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
ACM Transactions on Computational Logic | 2023-11-03 | Paper |
Preprocessing of propagation redundant clauses
Journal of Automated Reasoning | 2023-10-24 | Paper |
An automated approach to the Collatz conjecture
Journal of Automated Reasoning | 2023-06-27 | Paper |
An Impossible Asylum
The American Mathematical Monthly | 2023-05-11 | Paper |
SAT-Inspired Eliminations for Superposition
ACM Transactions on Computational Logic | 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
ACM Communications in Computer Algebra | 2023-01-11 | Paper |
| Preprocessing of propagation redundant clauses | 2022-12-07 | Paper |
The resolution of Keller's conjecture
Automated Reasoning | 2022-11-09 | Paper |
The resolution of Keller's conjecture
Journal of Automated Reasoning | 2022-10-24 | Paper |
Tighter bounds on directed Ramsey number \(R(7)\)
Graphs and Combinatorics | 2022-09-28 | Paper |
Skolem function continuation for quantified Boolean formulas
Tests and Proofs | 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
Artificial Intelligence | 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
(available as arXiv preprint) | 2021-12-01 | Paper |
| Odd-distance virtual edges in unit-distance graphs | 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
(available as arXiv preprint) | 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
Journal of Symbolic Computation | 2021-02-18 | Paper |
| Avoiding Monochromatic Rectangles Using Shift Patterns | 2020-12-23 | Paper |
Simulating strong practical proof systems with extended resolution
Journal of Automated Reasoning | 2020-11-02 | Paper |
Static detection of DoS vulnerabilities in programs that use regular expressions
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Truth assignments as conditional autarkies
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
Local search for fast matrix multiplication
(available as arXiv preprint) | 2020-05-20 | Paper |
| scientific article; zbMATH DE number 7178357 (Why is no real title available?) | 2020-03-09 | Paper |
Strong extension-free proof systems
Journal of Automated Reasoning | 2020-03-03 | Paper |
The implication problem of computing policies
Lecture Notes in Computer Science | 2020-01-14 | Paper |
Optimal symmetry breaking for graph problems
Mathematics in Computer Science | 2019-11-27 | Paper |
The Resolution of Keller's Conjecture
(available as arXiv preprint) | 2019-10-08 | Paper |
| What a difference a variable makes | 2019-09-16 | Paper |
Computing properties of stable configurations of thermodynamic binding networks
Theoretical Computer Science | 2019-07-31 | Paper |
| Trimming Graphs Using Clausal Proof Optimization | 2019-07-01 | Paper |
Computing small unit-distance graphs with chromatic number 5
(available as arXiv preprint) | 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
(available as arXiv preprint) | 2017-09-22 | Paper |
| Short proofs without new variables | 2017-09-22 | Paper |
Avoiding triples in arithmetic progression
Journal of Combinatorics | 2017-09-20 | Paper |
Solution validation and extraction for QBF preprocessing
Journal of Automated Reasoning | 2017-07-10 | Paper |
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Computing maximum unavoidable subgraphs using SAT solvers
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Reusing the assignment trail in CDCL solvers
Journal of Satisfiability, Boolean Modeling and Computation | 2016-02-23 | Paper |
Compositional propositional proofs
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Expressing symmetry breaking in DRAT proofs
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
A SAT approach to clique-width
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Clause elimination for SAT and QSAT
Journal of Artificial Intelligence Research | 2015-08-25 | Paper |
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
Lecture Notes in Computer Science | 2014-09-26 | Paper |
A unified proof system for QBF preprocessing
Automated Reasoning | 2014-09-26 | Paper |
MUS Extraction Using Clausal Proofs
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Everything you always wanted to know about blocked sets (but were afraid to ask)
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Symmetry in Gardens of Eden
The Electronic Journal of Combinatorics | 2014-08-14 | Paper |
Blocked clause decomposition
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
Mechanical verification of SAT refutations with extended resolution
Interactive Theorem Proving | 2013-08-07 | Paper |
A SAT approach to clique-width
Lecture Notes in Computer Science | 2013-08-05 | Paper |
Simulating circuit-level simplifications on CNF
Journal of Automated Reasoning | 2013-07-05 | Paper |
Verifying Refutations with Extended Resolution
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
Revisiting hyper binary resolution
Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems | 2013-06-04 | Paper |
Inprocessing rules
Automated Reasoning | 2012-09-05 | Paper |
Efficient CNF simplification based on binary implication graphs
Theory and Applications of Satisfiability Testing - SAT 2011 | 2011-06-17 | Paper |
Clause elimination procedures for CNF formulas
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Exact DFA Identification Using SAT Solvers
Grammatical Inference: Theoretical Results and Applications | 2010-09-10 | Paper |
Blocked clause elimination
Tools and Algorithms for the Construction and Analysis of Systems | 2010-04-27 | Paper |
Dynamic Symmetry Breaking by Simulating Zykov Contraction
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Effective Incorporation of Double Look-Ahead Procedures
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
From Idempotent Generalized Boolean Assignments to Multi-bit Search
Theory and Applications of Satisfiability Testing – SAT 2007 | 2009-03-10 | Paper |
| scientific article; zbMATH DE number 5510692 (Why is no real title available?) | 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
Discrete Applied Mathematics | 2008-09-10 | Paper |
Solving games dependence of applicable solving procedures
Science of Computer Programming | 2007-07-16 | Paper |
| March\_dl: adding adaptive heuristics and a new branching strategy | 2007-03-30 | Paper |
A new method to construct lower bounds for van der Waerden numbers
The Electronic Journal of Combinatorics | 2007-03-12 | Paper |
A new method to construct lower bounds for van der Waerden numbers
The Electronic Journal of Combinatorics | 2007-03-12 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2005-12-16 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2005-12-16 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2005-12-15 | Paper |
Happy Ending: An Empty Hexagon in Every Set of 30 Points
(available as arXiv preprint) | N/A | Paper |
PackIt! Gamified Rectangle Packing
(available as arXiv preprint) | N/A | Paper |
