31–40 of 46 posts
SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backtracking (mentioned in the article) is a thing in Prolog at least.
For instance, SICStus Prolog ships with a nice CLP(B) solver:
https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.ht...
This particular solver uses Binary Decision Diagrams (BDDs) to model and solve SAT instances.
CLP(B) blends in seamlessly with Prolog in the sense that Prolog variables and predicates are used to ask questions and obtain answers about satisfiability. For instance, we can formulate a Prolog query that asks: “Are there any X and Y such that the (X∧Y)∨X is satisfiable?”
?- sat(X*Y + X).
X = 1,
sat(Y=:=Y).
To obtain concrete assignments that make the expression true, we can use the library predicate labeling/1. On backtracking, all solutions are enumerated:
?- sat(X*Y + X), labeling([X,Y]).
X = 1, Y = 0 ;
X = Y, Y = 1.
http://www.gprolog.org/manual/html_node/gprolog061.html
The SAT solver of B-Prolog is so strong that it can compete with some dedicated SAT solvers. For a nice overview:
https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-pr...
A very nice SAT solver implementation in Prolog is explained in the paper A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King:
http://www.staff.city.ac.uk/~jacob/solver/flops.pdf
The paper shows that 20 lines of Prolog code suffice to implement an elegant solver for—as the authors put it—"solving some interesting, albeit modest, SAT instances".
However, SAT is a quite low-level way to encode combinatorial tasks, and for this reason, CLP(FD/ℤ), i.e., constraint logic programming over finite domains/integers is typically used instead of SAT when solving combinatorial tasks with Prolog.
Conceptually, we can think of CLP(ℤ) as a generalization of SAT solving, where variables can range over the entire integers instead of only 0 and 1. Strong and fast constraint solvers over integers are a major attraction of commercial Prolog systems, and often the key reason for buying one.
From a logical perspective, propositional logic can be regarded as a special case of first-order predicate logic, so a language rooted in predicate logic, like Prolog, is also related to SAT solving in this way.
SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results.
As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at.
They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck.
Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.
SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
These can be deployed against the Eternity II puzzle. I doubt any SAT solver will find a complete solution in our lifetimes, but a near solution would be satisfying. https://en.wikipedia.org/wiki/Eternity_II_puzzle
Heh.
https://news.ycombinator.com/item?id=19953213
Earlier quoted context omitted.
It is pretty easy to come up with an integer space in order to simulate week days, the concept of consecutiveness and homogeneous distribution. However, as soon as we get custom rules and exceptions things start to become impossible and we have to start inventing a best effort solution which turns into minimization or maximization of each human variable. At this point some humans with higher status want to be favoure…
> they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most comp…
Edit: well to be more specific, commitment is done with MIP solvers (difficult problem) and dispatch is done with LP solvers (easy and fast).
Earlier quoted context omitted.
> they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most comp…
... only a small subset know about MIP solvers And an even smaller subset are willing to pay to use gurobi or cplex. It would be so nice if the open source alternatives had competitive performance!