I've always been fascinated by how linear programming seems to be applicable to every problem under the sun but SAT solvers only really seem to be good at Sudoku.
In practice that are a bunch of problems that seem to be SAT, but they are either SAT at a scale where the solver still can't find a solution in any reasonable time or they turn out to not really be SAT because there is that one extra constraint that is quite difficult to encode in simple logic.
And it is unrewarding experimenting because it ends up being a day or so remembering how to use a SAT solver, then rediscovering how horrible raw sat solver interfaces are and trying to find a library that builds SAT problems from anything other than raw boolean algebra (the intros really undersell how bad the experience of using SAT solvers directly is, the DIMACS sat file format makes me think of the year 1973), then discovering that a SAT solver can't actually solve the alleged-SAT problem. Although if anyone is ever looking for a Clojure library I can recommend rolling-stones [0] as having a pleasant API to work with.
> ... SAT solvers only really seem to be good at Sudoku.
This is really not true.
SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
Because you can encode many (actually all) problems as a SAT instance, and the answer to that sat instance can be translated into an answer for the original problem.
Before you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer into your original domain language as you say).
Even simple goal-directed block's world-like robotic planning problems where the number of moves and the items to pickup/putdown are variable are much easier formulated and solved using Prolog.
SAT solvers are rarely used directly, they're usually a core component of a more expressive solver type like an LCG solver or an SMT solver.
And if not that, then they are used as the core component of a custom solver that speaks some higher level domain language.
Encoding things in CNF is a pain (even with higher level APIs like PySAT). But it's not usually something you should be doing unless you are developing a solver of some sort yourself.
When I've tried using SAT (or SMT) solvers I've had issues with scalability. The solution times, even if they didn't increase exponentially, tended to go up as some higher polynomial (like, cubic) in the size of the initial problems I was trying them on.
I love SAT solvers, but way more underappreciated by software engineers are MILP solvers.
MILPs (Mixed Integer Linear Programs) are basically sets of linear constraints, along with a linear optimization functions, where your variables can either be reals or ints.
Notably, you can easily encode any SAT problem as a MILP, but it's much easier to encode optimization problems, or problems with "county" constraints as MILPs.
Both are severely underused for sure. But it didn't help that for a long time open source MILP solvers were pretty mediocre.
HiGHS didn't exist, SCIP was "non-commercial", CBC was ok but they've been having development struggles for awhile, GLPK was never even remotely close to commercial offerings.
I think if something like Gurobi or Hexaly were open source, you'd see a lot more use since both their capabilities and performance are way ahead of the open source solutions, but it was the commercial revenue that made them possible in the first place.
Using CP-SAT from Google OR-Tools as a fake MILP solver by scaling the real variables is pretty funny though and works unreasonably well (specially if the problem is highly combinatorial since there's a SAT solver powering the whole thing)
SCIP going Apache definitely improved the landscape, but Couenne (global MINLP), Bonmin (local MINLP), and IPOPT (local NLP, but e.g. [1] gets you MINLP) are solid and have been around for a long time. And anecdotally, I've seen a lot more issues with SCIP (presolvers and tolerances, mostly) than with other solvers. Still it's replaced Couenne in my toolbox, and Minotaur has replaced Bonmin, but IPOPT remains king of its domain.
Many thanks to you and the parent comment for providing names to search when looking for implementations.
A basic question, before searching these: are they "input compatible"? I mean, can a problem be formulated once and then be solved by a variety of solvers? Or does each one of them use its own input language?
Didn't know about Randomized rounding. Is there any solver with built-in support for that? To turn a strong NLP solver into a fast but approximate MINLP solver?
SATs are cool but MILPs are cooler IMO.
Lol I've been trying to train a neural network over a finite field, not the reals and oh my god MILPs are God's gift to us.
If you get sick of MILPs, maybe you could use a representation of your finite field instead of the field itself? That way you could do everything in C^n, and preserve differentiability to use SGD or something like it.
If you convert a sudoku to an exact cover you can usually solve it by finding colums that are a subset from another column and remove all rows that are only in one of them.
Sudokus that can be solved with reasoning alone, can be solved in polynomial time.
I recently discovered that solving exact covers, and probably also with SAT, using a generic strategy, does not always result in the most efficient way for finding solutions. There are problems that have 10^50 solutions, yer finding a solution can take a long time.
Problems, including NP-complete ones, are only a product of the way you look at them and the reference frame from where you look at them. They get their incarnation only out of the observer's context.
Slightly related, there’s ways to differentiate linear programs (https://github.com/cvxpy/cvxpylayers), which might allow one to endow deep neural networks with some similar reasoning capabilities as these sorts of solvers.
I've always been fascinated by how linear programming seems to be applicable to every problem under the sun but SAT solvers only really seem to be good at Sudoku.
In practice that are a bunch of problems that seem to be SAT, but they are either SAT at a scale where the solver still can't find a solution in any reasonable time or they turn out to not really be SAT because there is that one extra constraint that is quite difficult to encode in simple logic.
And it is unrewarding experimenting because it ends up being a day or so remembering how to use a SAT solver, then rediscovering how horrible raw sat solver interfaces are and trying to find a library that builds SAT problems from anything other than raw boolean algebra (the intros really undersell how bad the experience of using SAT solvers directly is, the DIMACS sat file format makes me think of the year 1973), then discovering that a SAT solver can't actually solve the alleged-SAT problem. Although if anyone is ever looking for a Clojure library I can recommend rolling-stones [0] as having a pleasant API to work with.
[0] https://github.com/Engelberg/rolling-stones
> ... SAT solvers only really seem to be good at Sudoku.
This is really not true.
SAT solvers are really good these days, and many (exact) algorithms (for NP-hard problems) simply use some SOTA SAT solvers and are automatically competitive.
At doing what, though? Why are they solving the SAT problem?
Because you can encode many (actually all) problems as a SAT instance, and the answer to that sat instance can be translated into an answer for the original problem.
Before you go and try to encode "all problems as SAT instance", I'd recommend to consider that SAT formulations require a fixed number of (Boolean) variables. Sure, you can use tens of thousands of helper variables to encode a problem, but at a certain point this gets unwieldy and basically all you're doing is working around SAT limitations and spend your time implementing a SAT encoder (and translator for the answer into your original domain language as you say).
Even simple goal-directed block's world-like robotic planning problems where the number of moves and the items to pickup/putdown are variable are much easier formulated and solved using Prolog.
SAT solvers are rarely used directly, they're usually a core component of a more expressive solver type like an LCG solver or an SMT solver.
And if not that, then they are used as the core component of a custom solver that speaks some higher level domain language.
Encoding things in CNF is a pain (even with higher level APIs like PySAT). But it's not usually something you should be doing unless you are developing a solver of some sort yourself.
When I've tried using SAT (or SMT) solvers I've had issues with scalability. The solution times, even if they didn't increase exponentially, tended to go up as some higher polynomial (like, cubic) in the size of the initial problems I was trying them on.
I love SAT solvers, but way more underappreciated by software engineers are MILP solvers.
MILPs (Mixed Integer Linear Programs) are basically sets of linear constraints, along with a linear optimization functions, where your variables can either be reals or ints.
Notably, you can easily encode any SAT problem as a MILP, but it's much easier to encode optimization problems, or problems with "county" constraints as MILPs.
Both are severely underused for sure. But it didn't help that for a long time open source MILP solvers were pretty mediocre.
HiGHS didn't exist, SCIP was "non-commercial", CBC was ok but they've been having development struggles for awhile, GLPK was never even remotely close to commercial offerings.
I think if something like Gurobi or Hexaly were open source, you'd see a lot more use since both their capabilities and performance are way ahead of the open source solutions, but it was the commercial revenue that made them possible in the first place.
Using CP-SAT from Google OR-Tools as a fake MILP solver by scaling the real variables is pretty funny though and works unreasonably well (specially if the problem is highly combinatorial since there's a SAT solver powering the whole thing)
SCIP going Apache definitely improved the landscape, but Couenne (global MINLP), Bonmin (local MINLP), and IPOPT (local NLP, but e.g. [1] gets you MINLP) are solid and have been around for a long time. And anecdotally, I've seen a lot more issues with SCIP (presolvers and tolerances, mostly) than with other solvers. Still it's replaced Couenne in my toolbox, and Minotaur has replaced Bonmin, but IPOPT remains king of its domain.
1. E.g. https://en.wikipedia.org/wiki/Randomized_rounding.
Many thanks to you and the parent comment for providing names to search when looking for implementations.
A basic question, before searching these: are they "input compatible"? I mean, can a problem be formulated once and then be solved by a variety of solvers? Or does each one of them use its own input language?
Didn't know about Randomized rounding. Is there any solver with built-in support for that? To turn a strong NLP solver into a fast but approximate MINLP solver?
SATs are cool but MILPs are cooler IMO. Lol I've been trying to train a neural network over a finite field, not the reals and oh my god MILPs are God's gift to us.
Huh, that's an interesting idea.
If you get sick of MILPs, maybe you could use a representation of your finite field instead of the field itself? That way you could do everything in C^n, and preserve differentiability to use SGD or something like it.
If you convert a sudoku to an exact cover you can usually solve it by finding colums that are a subset from another column and remove all rows that are only in one of them.
Sudokus that can be solved with reasoning alone, can be solved in polynomial time.
I recently discovered that solving exact covers, and probably also with SAT, using a generic strategy, does not always result in the most efficient way for finding solutions. There are problems that have 10^50 solutions, yer finding a solution can take a long time.
Problems, including NP-complete ones, are only a product of the way you look at them and the reference frame from where you look at them. They get their incarnation only out of the observer's context.
Slightly related, there’s ways to differentiate linear programs (https://github.com/cvxpy/cvxpylayers), which might allow one to endow deep neural networks with some similar reasoning capabilities as these sorts of solvers.