Marijn J. H. Heule
YOU?
Author Swipe
View article: Unfolding Boxes with Local Constraints
Unfolding Boxes with Local Constraints Open
We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, including SAT, randomized algorithms, and decision diagrams, no…
View article: Automated Symmetric Constructions in Discrete Geometry
Automated Symmetric Constructions in Discrete Geometry Open
We present a computational methodology for obtaining rotationally symmetric sets of points satisfying discrete geometric constraints, and demonstrate its applicability by discovering new solutions to some well-known problems in combinatori…
View article: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers Open
View article: The Impact of Literal Sorting on Cardinality Constraint Encodings
The Impact of Literal Sorting on Cardinality Constraint Encodings Open
The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of…
View article: Certified Knowledge Compilation with Application to Formally Verified Model Counting
Certified Knowledge Compilation with Application to Formally Verified Model Counting Open
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision …
View article: Certified Knowledge Compilation with Application to Formally Verified Model Counting
Certified Knowledge Compilation with Application to Formally Verified Model Counting Open
Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision …
View article: Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification
Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification Open
Program verification languages such as Dafny and F $$ ^\star $$ often rely heavily on Satisfiability Modulo Theories (SMT) solvers for proof automation. However, SMT-based verification suffers from instability, where semantically irrele…
View article: Unfolding Boxes with Local Constraints
Unfolding Boxes with Local Constraints Open
We consider the problem of finding and enumerating polyominos that can be folded into multiple non-isomorphic boxes. While several computational approaches have been proposed, including SAT, randomized algorithms, and decision diagrams, no…
View article: Formal Verification of the Empty Hexagon Number
Formal Verification of the Empty Hexagon Number Open
A recent breakthrough in computer-assisted mathematics showed that every set of $30$ points in the plane in general position (i.e., without three on a common line) contains an empty convex hexagon, thus closing a line of research dating ba…
View article: PackIt! Gamified Rectangle Packing
PackIt! Gamified Rectangle Packing Open
We present and analyze PackIt!, a turn-based game consisting of packing rectangles on an $n \times n$ grid. PackIt! can be easily played on paper, either as a competitive two-player game or in \emph{solitaire} fashion. On the $t$-th turn, …
View article: Happy Ending: An Empty Hexagon in Every Set of 30 Points
Happy Ending: An Empty Hexagon in Every Set of 30 Points Open
Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein's exploration of una…
View article: Formal Verification of the Empty Hexagon Number
Formal Verification of the Empty Hexagon Number Open
A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem w…
View article: Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries (Short Paper)
Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries (Short Paper) Open
Envy-freeness up to any good (EFX) is a key concept in Computational Social Choice for the fair division of indivisible goods, where no agent envies another’s allocation after removing any single item. A deeper understanding of EFX allocat…
View article: TaSSAT: Transfer and Share SAT
TaSSAT: Transfer and Share SAT Open
We present , a powerful local search SAT solver that effectively solves hard combinatorial problems. Its unique approach of transferring clause weights in local minima enhances its efficiency in solving problem instances. Since it is imple…
View article: From Clauses to Klauses
From Clauses to Klauses Open
Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form. Cardinality constraints appear frequently in problem descriptions: over $$64\%$$ of the SAT Competition formulas cont…
View article: Happy Ending: An Empty Hexagon in Every Set of 30 Points
Happy Ending: An Empty Hexagon in Every Set of 30 Points Open
Satisfiability solving has been used to tackle a range of long-standing open math problems in recent years. We add another success by solving a geometry problem that originated a century ago. In the 1930s, Esther Klein’s exploration of una…
View article: Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane Open
We present a comprehensive demonstration of how automated reasoning can assist mathematical research, both in the discovery of conjectures and in their verification. Our focus is a discrete geometry problem: What is $μ_{5}(n)$, the minimum…
View article: The SAT Museum POS'23 Artifact
The SAT Museum POS'23 Artifact Open
<p>This dataset provides the artifact for our POS'23 paper on "The SAT Museum" effort. It includes the original sources of solvers winning the SAT competitions together with patches to fix, compile and run them with modern compilers,…
View article: The SAT Museum POS'23 Artifact
The SAT Museum POS'23 Artifact Open
This dataset provides the artifact for our POS'23 paper on "The SAT Museum" effort. It includes the original sources of solvers winning the SAT competitions together with patches to fix, compile and run them with modern compilers, as well …
View article: Preprocessing of Propagation Redundant Clauses
Preprocessing of Propagation Redundant Clauses Open
The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems t…
View article: Effective Auxiliary Variables via Structured Reencoding
Effective Auxiliary Variables via Structured Reencoding Open
Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (…
View article: Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Toward Optimal Radio Colorings of Hypercubes via SAT-solving Open
Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of tw…
View article: Generating Extended Resolution Proofs with a BDD-Based SAT Solver
Generating Extended Resolution Proofs with a BDD-Based SAT Solver Open
In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical …
View article: An Automated Approach to the Collatz Conjecture
An Automated Approach to the Collatz Conjecture Open
We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binar…
View article: A Linear Weight Transfer Rule for Local Search
A Linear Weight Transfer Rule for Local Search Open
The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic local search SAT-solving algorithm that transfers weight from satisfied to falsified clauses in local minima. ddfw is remarkably effective on several hard combinatorial …
View article: Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML Open
Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy ( $$\textsf{PR}$$ ). However, the on…
View article: An Impossible Asylum
An Impossible Asylum Open
In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last…
View article: The Packing Chromatic Number of the Infinite Square Grid is 15
The Packing Chromatic Number of the Infinite Square Grid is 15 Open
A packing $k$-coloring is a natural variation on the standard notion of graph $k$-coloring, where vertices are assigned numbers from $\{1, \ldots, k\}$, and any two vertices assigned a common color $c \in \{1, \ldots, k\}$ need to be at a …
View article: The Packing Chromatic Number of the Infinite Square Grid is 15
The Packing Chromatic Number of the Infinite Square Grid is 15 Open
A packing k -coloring is a natural variation on the standard notion of graph k -coloring, where vertices are assigned numbers from $$\{1, \ldots , k\}$$ , and any two vertices assigned a common color $$c \in \{1, \ldots , k\}$$ …
View article: Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers Open
Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, h…