Zobrazeno 1 - 10
of 164
pro vyhledávání: '"Heule, Marijn"'
Autor:
Subercaseaux, Bernardo, Nawrocki, Wojciech, Gallicchio, James, Codel, Cayden, Carneiro, Mario, Heule, Marijn J. H.
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 back to the 1
Externí odkaz:
http://arxiv.org/abs/2403.17370
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, a rectangle
Externí odkaz:
http://arxiv.org/abs/2403.12195
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 unavoidable sh
Externí odkaz:
http://arxiv.org/abs/2403.00737
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 $\mu_{5}(n)$, the minimum number o
Externí odkaz:
http://arxiv.org/abs/2311.03645
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 (BVA), which
Externí odkaz:
http://arxiv.org/abs/2307.01904
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 instances.
Externí odkaz:
http://arxiv.org/abs/2303.14894
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 distance gr
Externí odkaz:
http://arxiv.org/abs/2301.09757
Autor:
Yolcu, Emre, Heule, Marijn J. H.
We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula $\Gamma$ in conjunctive normal form, deriving clauses that are not necessarily logically implied by $\Gamma$ but whose addition to $\Gamma
Externí odkaz:
http://arxiv.org/abs/2211.12456
The Pigeonhole Principle (PHP) has been heavily studied in automated reasoning, both theoretically and in practice. Most solvers have exponential runtime and proof length, while some specialized techniques achieve polynomial runtime and proof length.
Externí odkaz:
http://arxiv.org/abs/2207.11284