DIR Return Create A Forum - Home
---------------------------------------------------------
knight tours
HTML https://knighttours.createaforum.com
---------------------------------------------------------
*****************************************************
DIR Return to: general Hamiltonian cycles problem
*****************************************************
#Post#: 19--------------------------------------------------
SAT-solver
By: gsgs Date: June 26, 2023, 9:38 pm
---------------------------------------------------------
-----------edit------update 2025-12-30------------------
ganak2 "model-counting"
best for counting all solutions of a SAT-instance
HTML https://github.com/meelgroup/ganak/releases/tag/release%2F2.5.2
--------edit , update :--------
kissat 4.0 is here :
HTML https://github.com/arminbiere/kissat/releases/tag/rel-4.0.0
kissat :
HTML https://github.com/arminbiere/kissat
awfully complicated, >180 files of source-code
Ubuntu executable which worked for me :
HTML https://github.com/simewu/top-SAT-solvers-2021/blob/main/kissat_gb/build/kissat
This is kissat_gp (whatever that means) , kissat-mpd doesn't run
on my
system
for Hamiltonian cycle you need to modify it, so it prints all
solutions,
not just one. It should be simple, but I see no easy way
to change the source-code accordingly.
And you have to convert HC to SAT-CNF.
so far I used a simple conversion to find all cycle-coverings
as exact cover and "pairwise" to convert exact cover to SAT
HTML http://magictour.free.fr/dlx2sat.c
#Post#: 20--------------------------------------------------
Re: SAT-solver
By: gsgs Date: July 27, 2023, 1:40 am
---------------------------------------------------------
2020-paper :
In pursuit of an efficient SAT encoding for the Hamiltonian
cycle problem
HTML http://www.picat-lang.org/papers/cp20.pdf
knight's tour instances for the 2019 XCSP competition
for SAT-solvers :
HTML https://www.cril.univ-artois.fr/XCSP19/results/globalbybench.php?idev=99&idcat=0
Knights/ Knights-m1-s1/ Knights-015-09.xml
Knights/ Knights-m1-s1/ Knights-080-25.xml
KnightTour/ KnightTour-ext-s1/ KnightTour-08-ext03.xml
KnightTour/ KnightTour-ext-s1/ KnightTour-12-ext04.xml
KnightTour/ KnightTour-ext-s1/ KnightTour-15-ext06.xml
knightTour/ KnightTour-ext-s1/ KnightTour-17-ext02.xml
KnightTour/ KnightTour-int-s1/ KnightTour-05-int.xml
KnightTour/ KnightTour-int-s1/ KnightTour-08-int.xml
KnightTour/ KnightTour-int-s1/ KnightTour-17-int.xml
QueensKnights/ QueensKnights-m1-s1/ QueensKnights-050-05-mul.xml
QueensKnights/ QueensKnights-m1-s1/ QueensKnights-080-05-add.xml
hcp-problems :
162,171,197,223,237,249,252,254,255,48,
HTML https://www.cril.univ-artois.fr/XCSP19/results/bench.php?idev=99&idbench=134620
HTML https://www.cril.univ-artois.fr/XCSP19/results/bench.php?idev=99&idbench=141698
graph223 :
HTML https://www.cril.univ-artois.fr/XCSP19/results/bench.php?idev=99&idbench=141691
chalat solves graph223 in 22s, complete search (4HCs) in 318s
vacul solves it in 3s (,first H ; complete search not supported)
with border-reorder : chalat solves it in 1s,2s ; vacul in
20s,-
----------------------------------------------------------------
---
HTML https://wvvw.easychair.org/publications/preprint_download/pp38
[PDF] Stedman and Erin triples encoded as a SAT problem
A Johnson - Federated Logic Conference, 2018 -
wvvw.easychair.org
very efficient general reduction of the Hamiltonian Cycle
Problem (HCP) to (SAT)
converting any Hamiltonian Cycle problem with n vertices and m
directed edges
to a SAT problem with approximately
n*log_2(m) variables and 2*m*(log_2(n)+1) clauses.
n=1000,m=1500 ==> 10000 variables 33000 clauses
n=64,m=168 (knight 8x8) ==> 473 variables , 2352 clauses
(the conversion program is apparently not available)
The big problem with encoding Hamiltonian cycle type problems
into SAT is enforcing the only one loop requirement.
There have been a variety of approaches to the problem,
including Iwama[8], Creignou[1]
who saw HCP as SAT-hard but not SAT-easy,
Plottikov[17], Nasu[16], Prestwich[18], Soh[26],
Velev and Gao[31][33][32].
old : n^2 variables and n^3 clauses
A search of graph479=Sted10 finds a solution takes
2611 seconds (Glucose) or
21 seconds (MiniSat)
Erin3 and Sted5 can be searched and proved UNSAT
by a supercomputer cluster over a period of a week or two.
A complete search of Sted5 was completed in less than a week
(Glucose) on the Flinders University Colossus supercomputer
with over 1000 nodes.
-------------------------------------------------------
*****************************************************