research
∙
07/04/2023
Effective Auxiliary Variables via Structured Reencoding
Extended resolution shows that auxiliary variables are very powerful in ...
share
research
∙
03/27/2023
A Linear Weight Transfer Rule for Local Search
The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic lo...
research
∙
01/23/2023
The Packing Chromatic Number of the Infinite Square Grid is 15
A packing k-coloring is a natural variation on the standard notion of gr...
research
∙
11/22/2022
Exponential separations using guarded extension variables
We study the complexity of proof systems augmenting resolution with infe...
research
∙
07/22/2022
Towards the shortest DRAT proof of the Pigeonhole Principle
The Pigeonhole Principle (PHP) has been heavily studied in automated rea...
research
∙
09/20/2021
A Flexible Proof Format for SAT Solver-Elaborator Communication
We introduce FRAT, a new proof format for unsatisfiable SAT problems, an...
research
∙
05/31/2021
An Automated Approach to the Collatz Conjecture
We explore the Collatz conjecture and its variants through the lens of t...
research
∙
05/03/2021
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
In 2006, Biere, Jussila, and Sinz made the key observation that the unde...
research
∙
09/21/2020
Modeling Techniques for Logic Locking
Logic locking is a method to prevent intellectual property (IP) piracy. ...
research
∙
07/01/2019
Trimming Graphs Using Clausal Proof Optimization
We present a method to gradually compute a smaller and smaller unsatisfi...
research
∙
07/01/2019
Computing a Smaller Unit-Distance Graph with Chromatic Number 5 via Proof Trimming
We present a method to gradually compute a smaller and smaller unsatisfi...
research
∙
05/24/2019
New ways to multiply 3 x 3-matrices
It is known since the 1970s that no more than 23 multiplications are req...
research
∙
03/27/2019
Local Search for Fast Matrix Multiplication
Laderman discovered a scheme for computing the product of two 3x3 matric...
research
∙
11/21/2017
Schur Number Five
We present the solution of a century-old problem known as Schur Number F...
research
∙
02/18/2014