Index of /~waldmann/sat/leaper

Name	Last modified	Size

Parent Directory		-
README.html	2023-11-13 09:29	3.8K
README.md	2023-11-13 09:29	2.9K
giraffe-11.cnf.xz	2023-11-13 09:15	522K

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:

exactly-one uses Jingchao Chen: A New SAT Encoding of the At-Most-One Constraint, 10th Workshop Constraint Modeling and Reformulation, 2010
“at least one of the 8 neighbours”: we could write “exactly one” here, but don’t, to keep the formula smaller

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