Reduction from dancing links instance to SAT instance

[slabbe]

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.

[git]

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

​c368cc1

29338: reduction from DLX to SAT

[mkoeppe]

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]

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.

[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

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

[slabbe]

See #29955 for the reduction to MILP.

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

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

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

[saliola]

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

Thank you, Sébastien!

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

[slabbe]

Thanks for the review!