The
(1,4) Leaper Graph on 11 x 11 has no Hamiltonian Path
this solves an open problem, see Eric Weisstein: Giraffe Graph, https://mathworld.wolfram.com/GiraffeGraph.html. For
background, George Jellis: Leapers At Large, 2001 http://www.mayhematics.com/t/pl.htm#(3)
naive SAT-encoding
- unknowns: Boolean matrix B that represents a bijection between place
(11 x 11) and time (0 .. 120). Total: 11^4 = 14.641 unknowns
- constraints:
- matrix is bijection (for each row, and each column, an exactly-one
constraint)
- path fits the graph: for each time t, and position p, at least one
of the 8 neighbours at time t-1, and of those at time t+1, is one jump
away from p
Notes on encoding:
Notes on
producing the encoding programmatically:
- we use Kmett, Mertens, Scott: https://hackage.haskell.org/package/ersatz to produce
(essentially) a circuit (DAG) and Tseitin transforme it. Resulting CNF
has 48.765 variables, 438.354 clauses, compressed 648.748 bytes
- is reduced to 18.029 variables, 240.790 clauses, 788.526 literals by
minisat (Niklas Eén, Niklas Sörensson)
preprocessing, and similarly, or better, with other solvers. This is
pretty good, considering the number of actual unknowns (11^4)
Solving and Verification
- kissat (Armin
Biere) says UNSAT after approx. 10 hours, produces proof trace of
29.616.172.097 bytes (binary, uncompressed), compresses 9.655.166.616 bytes
- drat-trim
(Marijn Heule) checks this in approx. 10 hours
Actual Verifier Output
[waldmann@16tons drat-trim]$ time ./drat-trim ~/skript/cp/code/amo/giraffe-11.cnf ~/skript/cp/code/amo/giraffe-11.proof -b
c turning on binary mode checking
c parsing input formula with 48765 variables and 438354 clauses
c finished parsing, read 29616172097 bytes from proof file
c detected empty clause; start verification via backward checking
c 3.19% [ ] time remaining: 58526.85 c 3.19% [ ] time remaining: 58522.24 c c 218277 of 438354 clauses in core
c 40402019 of 115138111 lemmas in core using 37235537285 resolution steps
c 0 RAT lemmas in core; 87232443 redundant literals in core lemmas
s VERIFIED
c verification time: 31714.221 seconds
real 528m35.686s
user 526m34.388s
sys 0m22.266s
Similar open problems
does a Hamiltonian Path exist for