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

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

Authors: | → Sébastien Labbé |
---|---|

Branch: | → u/slabbe/29338 |

Commit: | → 87c3057957495ee3ff135e88f792151b8c89cea9 |

Status: | new → needs_review |

### comment:2 Changed 3 years ago by

Commit: | 87c3057957495ee3ff135e88f792151b8c89cea9 → c368cc170ed7d08a5d6bf35d25f14c18d627bb3a |
---|

### comment:3 Changed 3 years ago by

Milestone: | sage-9.1 → 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: | c368cc170ed7d08a5d6bf35d25f14c18d627bb3a → 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: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 #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

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

Status: | needs_review → 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 Changed 2 years ago by

[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:15 Changed 2 years ago by

Branch: | u/slabbe/29338 → 2e97345c41638ae8be5d8d7cac2737300883dfcf |
---|---|

Resolution: | → fixed |

Status: | positive_review → closed |

**Note:**See TracTickets for help on using tickets.

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

`29338: reduction from DLX to SAT`