Opened 2 years ago
Closed 2 years ago
#29338 closed enhancement (fixed)
Reduction from dancing links instance to SAT instance
Reported by: | slabbe | Owned by: | |
---|---|---|---|
Priority: | major | Milestone: | sage-9.2 |
Component: | combinatorics | Keywords: | |
Cc: | Merged in: | ||
Authors: | Sébastien Labbé | Reviewers: | Franco Saliola |
Report Upstream: | N/A | Work issues: | |
Branch: | 2e97345 (Commits, GitHub, GitLab) | Commit: | 2e97345c41638ae8be5d8d7cac2737300883dfcf |
Dependencies: | Stopgaps: |
Description
The proposed branch adds 2 new methods which allows what follows:
sage: from sage.combinat.matrices.dancing_links import dlx_solver sage: rows = [[0,1,2], [3,4,5], [0,1], [2,3,4,5], [0], [1,2,3,4,5]] sage: d = dlx_solver(rows) sage: d.one_solution() [1, 0] sage: d.one_solution_using_sat_solver('cryptominisat') [2, 3] sage: d.one_solution_using_sat_solver('glucose') [2, 3] sage: d.one_solution_using_sat_solver('glucose-syrup') [2, 3] sage: d.one_solution_using_sat_solver('picosat') [4, 5] sage: d.one_solution_using_sat_solver('LP') [2, 3] sage: d.one_solution_using_sat_solver() [2, 3]
This is based on the new method:
sage: d.to_sat_solver() CryptoMiniSat solver: 6 variables, 24 clauses.
Change History (15)
comment:1 Changed 2 years ago by
- Branch set to u/slabbe/29338
- Commit set to 87c3057957495ee3ff135e88f792151b8c89cea9
- Status changed from new to needs_review
comment:2 Changed 2 years ago by
- Commit changed from 87c3057957495ee3ff135e88f792151b8c89cea9 to c368cc170ed7d08a5d6bf35d25f14c18d627bb3a
comment:3 Changed 2 years ago by
- Milestone changed from sage-9.1 to sage-9.2
Batch modifying tickets that will likely not be ready for 9.1, based on a review of the ticket title, branch/review status, and last modification date.
comment:4 Changed 2 years ago by
This is really nice. Only one suggestion: make it so that one_solution
and one_solution_using_sat_solver
handle the case of no solutions consistently. The former returns None
whereas the latter raises a ValueError
in case there is no solution.
Personally, I prefer None
since I can easily write if soln is None: ...
instead of a try/except
.
comment:5 Changed 2 years ago by
- Commit changed from c368cc170ed7d08a5d6bf35d25f14c18d627bb3a to 2e97345c41638ae8be5d8d7cac2737300883dfcf
comment:6 Changed 2 years ago by
I rebased on top of a more recent version of Sage. Needs review. I will implement one_solution_using_milp_solver
in another ticket, probably on top of that branch to avoid conflicts.
comment:7 Changed 2 years ago by
See #29955 for the reduction to MILP.
comment:8 Changed 2 years ago by
A question about the interface. Since we are going to have:
one_solution
one_solution_using_sat_solver
one_solution_using_milp_solver
# with #29955
I think it would it be better to have only one method that dispatches to the various solvers. Then one can do the following:
one_solution(solver="dlx")
one_solution(solver="cryptominisat")
one_solution(solver="picosat")
one_solution(solver="Gurobi")
# with #29955one_solution(solver="CLPLEX")
# with #29955
What do you think? (I can do this if you think it is a good idea.)
comment:9 Changed 2 years ago by
I made that choice to make it explicit that we are not using the dlx solver (we can not compare timing (at least on the first call) for example, because of the initialization of the rows is already done when using "dlx") and to make explicit that there is a overhead in doing the translation of the thousands of rows into something else.
I think one_solution(solver='Gurobi')
should not be something so much desirable, since if this is really what is the most efficient, then one should just construct the MILP
directly.
What do you think is best to do?
comment:10 follow-up: ↓ 13 Changed 2 years ago by
Ah, this is a very good point! So I should think of the principal goal of this ticket as the implementation of to_sat_solver
, and one_solution_using_sat_solver
is a shortcut for the following:
sage: d.to_sat_solver('glucose').solve() # not the correct syntax; see below
[Note that solve
is not a method for sat
; the above should be d.to_sat_solver('glucose')()
instead.]
comment:11 Changed 2 years ago by
- Reviewers set to Franco Saliola
- Status changed from needs_review to positive_review
comment:12 Changed 2 years ago by
All doctests pass, including the optional doctests with 'glucose', 'picosat', etc.
Thank you, Sébastien!
comment:13 in reply to: ↑ 10 Changed 2 years ago by
[Note that
solve
is not a method forsat
; the above should bed.to_sat_solver('glucose')()
instead.]
But this is not enough, because one need to translate the solution of the SAT problem into a solution to a DLX problem...
comment:14 Changed 2 years ago by
Thanks for the review!
comment:15 Changed 2 years ago by
- Branch changed from u/slabbe/29338 to 2e97345c41638ae8be5d8d7cac2737300883dfcf
- Resolution set to fixed
- Status changed from positive_review to closed
Branch pushed to git repo; I updated commit sha1. New commits:
29338: reduction from DLX to SAT