#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:

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 20 months ago by slabbe

  • Authors set to Sébastien Labbé
  • Branch set to u/slabbe/29338
  • Commit set to 87c3057957495ee3ff135e88f792151b8c89cea9
  • Status changed from new to needs_review

comment:2 Changed 20 months ago by git

  • Commit changed from 87c3057957495ee3ff135e88f792151b8c89cea9 to c368cc170ed7d08a5d6bf35d25f14c18d627bb3a

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

c368cc129338: reduction from DLX to SAT

comment:3 Changed 19 months ago by mkoeppe

  • 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 16 months ago by 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 16 months ago by git

  • Commit changed from c368cc170ed7d08a5d6bf35d25f14c18d627bb3a to 2e97345c41638ae8be5d8d7cac2737300883dfcf

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 16 months ago by slabbe

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 16 months ago by slabbe

See #29955 for the reduction to MILP.

comment:8 Changed 16 months ago by 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 16 months ago by slabbe

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 16 months ago by slabbe (previous) (diff)

comment:10 follow-up: Changed 16 months ago by 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 16 months ago by saliola

  • Reviewers set to Franco Saliola
  • Status changed from needs_review to positive_review

comment:12 Changed 16 months ago by saliola

All doctests pass, including the optional doctests with 'glucose', 'picosat', etc.

Thank you, Sébastien!

comment:13 in reply to: ↑ 10 Changed 16 months ago by slabbe

[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 16 months ago by slabbe

Thanks for the review!

comment:15 Changed 16 months ago by vbraun

  • Branch changed from u/slabbe/29338 to 2e97345c41638ae8be5d8d7cac2737300883dfcf
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.