Opened 3 years ago

Closed 2 years ago

#29338 closed enhancement (fixed)

Reduction from dancing links instance to SAT instance

Reported by: Sébastien Labbé 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:

Status badges

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 3 years ago by Sébastien Labbé

Authors: Sébastien Labbé
Branch: u/slabbe/29338
Commit: 87c3057957495ee3ff135e88f792151b8c89cea9
Status: newneeds_review

comment:2 Changed 3 years ago by git

Commit: 87c3057957495ee3ff135e88f792151b8c89cea9c368cc170ed7d08a5d6bf35d25f14c18d627bb3a

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

c368cc129338: reduction from DLX to SAT

comment:3 Changed 3 years ago by Matthias Köppe

Milestone: sage-9.1sage-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 Franco Saliola

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 git

Commit: c368cc170ed7d08a5d6bf35d25f14c18d627bb3a2e97345c41638ae8be5d8d7cac2737300883dfcf

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

542c3fc29338: reduction from DLX to SAT
2e9734529338:return None if no solution found

comment:6 Changed 2 years ago by Sébastien Labbé

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 Sébastien Labbé

See #29955 for the reduction to MILP.

comment:8 Changed 2 years ago by Franco Saliola

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 #29955
  • one_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 Sébastien Labbé

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?

Last edited 2 years ago by Sébastien Labbé (previous) (diff)

comment:10 Changed 2 years ago by Franco Saliola

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 Franco Saliola

Reviewers: Franco Saliola
Status: needs_reviewpositive_review

comment:12 Changed 2 years ago by Franco Saliola

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 Sébastien Labbé

[Note that solve is not a method for sat; the above should be d.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 Sébastien Labbé

Thanks for the review!

comment:15 Changed 2 years ago by Volker Braun

Branch: u/slabbe/293382e97345c41638ae8be5d8d7cac2737300883dfcf
Resolution: fixed
Status: positive_reviewclosed
Note: See TracTickets for help on using tickets.