3 ms·

Beautiful. This is exactly what I was hoping to see. This sub-link is especially good. https://alexpeattie.com/blog/establishing-minimum-guesses-wordle/ https:

Beautiful. This is exactly what I was hoping to see. This sub-link is especially good. https://alexpeattie.com/blog/establishing-minimum-guesses-wordle/ https://alexpeattie.com/blog/establishing-minimum-guesses-wo... I really really need to learn how to use an SAT solver. The problems they can solve is downright magical as far as I’m concerned. Does anyone know of some good tutorials?

lacker 5y ago
It probably really depends what sort of problem you're working on, but in my experience it was easier to represent things as mixed integer linear programming, (MIP) rather than a SAT instance. They're both NP-complete representations, but with the MIP representation you can naturally add constraints like "maximize the sum of these various things" as well as the sort of boolean constraints that work naturally with SAT. And for MIP solving, the Python mip package is quite convenient. https://python-mip.readthedocs.io/en/latest/quickstart.html https://python-mip.readthedocs.io/en/latest/quickstart.html
CJefferson 5y ago
I would strongly recommend using minizinc ( https://www.minizinc.org/ https://www.minizinc.org/ ) or Essence ( https://conjure.readthedocs.io/en/latest/essence.html https://conjure.readthedocs.io/en/latest/essence.html ) (other systems exist too), which provide higher-level interfaces to SAT (and other system) solving. You can view these as compilers to SAT, much like "no-one writes in assembler", most people don't write raw SAT either :)
mzl 5y ago
I agree with the recommendation to start with a modelling language in a sibling comment. On the MiniZinc homepage, there are Coursera courses linked that are quite nice as an introduction into combinatorial modelling. Apart from that, it is worth noting that the solver used in the article, OR-Tools, is not strictly a SAT solver. I would rather describe it as a hybrid portfolio solver, since it combines constraint programming, SAT, MIP, and local search in a single solver. It is also possible to use that solver as a back-end when solving a model written in MiniZinc.

lacker 5y ago

It probably really depends what sort of problem you're working on, but in my experience it was easier to represent things as mixed integer linear programming, (MIP) rather than a SAT instance. They're both NP-complete representations, but with the MIP representation you can naturally add constraints like "maximize the sum of these various things" as well as the sort of boolean constraints that work naturally with SAT. And for MIP solving, the Python mip package is quite convenient. https://python-mip.readthedocs.io/en/latest/quickstart.html https://python-mip.readthedocs.io/en/latest/quickstart.html

CJefferson 5y ago

I would strongly recommend using minizinc ( https://www.minizinc.org/ https://www.minizinc.org/ ) or Essence ( https://conjure.readthedocs.io/en/latest/essence.html https://conjure.readthedocs.io/en/latest/essence.html ) (other systems exist too), which provide higher-level interfaces to SAT (and other system) solving. You can view these as compilers to SAT, much like "no-one writes in assembler", most people don't write raw SAT either :)

mzl 5y ago

I agree with the recommendation to start with a modelling language in a sibling comment. On the MiniZinc homepage, there are Coursera courses linked that are quite nice as an introduction into combinatorial modelling. Apart from that, it is worth noting that the solver used in the article, OR-Tools, is not strictly a SAT solver. I would rather describe it as a hybrid portfolio solver, since it combines constraint programming, SAT, MIP, and local search in a single solver. It is also possible to use that solver as a back-end when solving a model written in MiniZinc.