Reduction from dancing links instance to SAT instance

[seblabbe]

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.

Component: combinatorics

Author: Sébastien Labbé

Branch/Commit: 2e97345

Reviewer: Franco Saliola

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

[seblabbe]

Author: Sébastien Labbé

[seblabbe]

Branch: u/slabbe/29338

[seblabbe]

Commit: 87c3057

[sagetrac-git]

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

c368cc1

29338: reduction from DLX to SAT

[sagetrac-git]

Changed commit from 87c3057 to c368cc1

[mkoeppe]

comment:3

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.

[saliola]

comment:4

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.

[sagetrac-git]

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

542c3fc	29338: reduction from DLX to SAT
2e97345	29338:return None if no solution found

[sagetrac-git]

Changed commit from c368cc1 to 2e97345

[seblabbe]

comment:6

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.

[seblabbe]

comment:7

See #29955 for the reduction to MILP.

[saliola]

comment:8

A question about the interface. Since we are going to have:

• one_solution
• one_solution_using_sat_solver
• one_solution_using_milp_solver # with Reduction from dancing links instance to MILP instance #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 Reduction from dancing links instance to MILP instance #29955
• one_solution(solver="CLPLEX") # with Reduction from dancing links instance to MILP instance #29955
  What do you think? (I can do this if you think it is a good idea.)

[seblabbe]

comment:9

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?

[saliola]

comment:10

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.]

[saliola]

Reviewer: Franco Saliola

[saliola]

comment:12

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

Thank you, Sébastien!

[seblabbe]

comment:13

[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...

[seblabbe]

comment:14

Thanks for the review!

[vbraun]

Changed branch from u/slabbe/29338 to 2e97345