Adding class Kissat in sage/sat/solvers/dimacs.py

[seblabbe]

We add a class Kissat in sage/sat/solvers/dimacs.py

We also use the opportunity to improve the dimacs.py file (uniformize the classes so that they can inherit the same __call__ method, added documentation and new doctests).

This is a follow up of #34909.

Depends on #34909

Component: packages: optional

Author: Sébastien Labbé

Branch/Commit: 27a3125

Reviewer: Andrey Belgorodski

Issue created by migration from https://trac.sagemath.org/ticket/34911

[seblabbe]

Last 10 new commits:

8262dcd	using just a spkg-install.in with no spkg-build.in
ae36201	build/pkgs/kissat/SPKG.rst: Fix title format, remove empty section
cea9e49	build/pkgs/kissat: Fix scripts
a991372	build/pkgs/kissat/distros: Add more
1ad4eb0	renaming DIMACS.__call__ as DIMACS._run; moving RSat.__call__ up to parent DIMACS.__call__; improved doc
0203eb3	Adding class Kissat
7f0b65e	Improved the output parsing in __call__
c748add	Adding kissat to SAT list of options
3d71886	Using -model for Glucose command so that the format of the output have same format (starting with letter v)
18364bf	making the `__call__` work whatever the DIMACS SAT solver

[seblabbe]

Branch: u/slabbe/34911

[seblabbe]

Commit: 18364bf

[seblabbe]

Dependencies: #34909

[seblabbe]

Author: Sébastien Labbé

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

961719c

making doctests solution indenpendent

[sagetrac-git]

Changed commit from 18364bf to 961719c

[seblabbe]

comment:5

My sage -t command is currently broken, so maybe not all tests pass. This is why I wait before setting the status to needs review.

[sheerluck]

comment:6

1. sat/solvers/dimacs.py # Tab character found

File "sage/sat/solvers/dimacs.py", lines 535, 572, 640, 707 
Expected: DIMACS Solver: 'rsat {input} {output} -v -s' 
Got:      DIMACS Solver: 'rsat {input} -v -s' 
Expected: DIMACS Solver: 'glucose -verb=2 {input} {output}'
Got:      DIMACS Solver: 'glucose -verb=0 -model {input}'
Expected: DIMACS Solver: 'glucose-syrup -model -verb=2 {input}'
Got:      DIMACS Solver: 'glucose-syrup -model -verb=0 {input}'
Expected: DIMACS Solver: 'kissat {input} {output}'
Got:      DIMACS Solver: 'kissat -q {input}'

File "sage/sat/solvers/satsolver.pyx", line 364, 369, 374 
Expected: DIMACS Solver: 'glucose -verb=2 {input} {output}'
Got:      DIMACS Solver: 'glucose -verb=0 -model {input}'
Expected: DIMACS Solver: 'glucose-syrup -model -verb=2 {input}'
Got:      DIMACS Solver: 'glucose-syrup -model -verb=0 {input}'
Expected: DIMACS Solver: 'kissat -q {input} {output}'
Got:      DIMACS Solver: 'kissat -q {input}'

3. without --optional=glucose,kissat

[148 tests, 0.19 s]

4. with --optional=glucose,kissat

[172 tests, 1.71 s]

[sagetrac-git]

Changed commit from 961719c to 27a3125

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

c02693d	34909: removed line 'mkdir build' in spkg-install
0d2f088	renaming DIMACS.__call__ as DIMACS._run; moving RSat.__call__ up to parent DIMACS.__call__; improved doc
93b12a6	Adding class Kissat
ba249f6	Improved the output parsing in __call__
b1e287d	Adding kissat to SAT list of options
f97dacc	Using -model for Glucose command so that the format of the output have same format (starting with letter v)
c21a080	making the `__call__` work whatever the DIMACS SAT solver
6e7dfb7	making doctests solution indenpendent
b55a0b9	34911: removed tabulation, fixed doctests
27a3125	34911: fixing doc build

[seblabbe]

comment:8

Thanks for the list. Meanwhile I fixed my sage -t after doing make distclean.

Rebased on top of the additional commit which was made in #34909.

Fixed tabulation, doctests and docbuild. Needs review!

[seblabbe]

comment:9

With sage -pip install slabbe done, I can now expand the comparison of solvers solving the tiling of a n times n square by Wang tiles:

sage: from slabbe import WangTileSet
sage: tiles = [(2,4,2,1), (2,2,2,0), (1,1,3,1), (1,2,3,2), (3,1,3,3),
....: (0,1,3,1), (0,0,0,1), (3,1,0,2), (0,2,1,2), (1,2,1,4), (3,3,1,2)]
sage: T0 = WangTileSet([tuple(str(a) for a in t) for t in tiles])

With glucose:

sage: %time T0.solver(55,55).solve(solver='glucose')
CPU times: user 1.53 s, sys: 12 ms, total: 1.54 s
Wall time: 7.07 s
A wang tiling of a 55 x 55 rectangle
sage: %time T0.solver(60,60).solve(solver='glucose')
CPU times: user 1.79 s, sys: 23.9 ms, total: 1.82 s
Wall time: 13.3 s
A wang tiling of a 60 x 60 rectangle

With kissat:

sage: %time T0.solver(55,55).solve(solver='kissat')
CPU times: user 1.53 s, sys: 19.7 ms, total: 1.55 s
Wall time: 8.84 s
A wang tiling of a 55 x 55 rectangle
sage: %time T0.solver(60,60).solve(solver='kissat')
CPU times: user 1.84 s, sys: 27.9 ms, total: 1.87 s
Wall time: 14.8 s
A wang tiling of a 60 x 60 rectangle

It turns out kissat is comparable but not better than glucose for this question.

Anyway, this is just to confirm the code here works.

[seblabbe]

comment:12

Thanks for the review!

Please add your complete name to the Reviewer field, as otherwise the release manager will change the status to "needs work".

[sheerluck]

Reviewer: Andrey Belgorodski

[vbraun]

Changed branch from u/slabbe/34911 to 27a3125