Closed seblabbe closed 1 year ago
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 |
Branch: u/slabbe/34911
Dependencies: #34909
Author: Sébastien Labbé
Branch pushed to git repo; I updated commit sha1. New commits:
961719c | making doctests solution indenpendent |
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.
1) sat/solvers/dimacs.py # Tab character found
2)
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]
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 |
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!
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.
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".
Reviewer: Andrey Belgorodski
Changed branch from u/slabbe/34911 to 27a3125
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