You can also watch the talk from same author about the same subject here - https://www.youtube.com/watch?v=x2XtpCn0-bM
Modern SAT solvers: fast, neat and underused
21–30 of 46 posts
Re: Modern SAT solvers: fast, neat and underused
#22SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3].
[1] https://ucsd-progsys.github.io/liquidhaskell-blog/
Re: Modern SAT solvers: fast, neat and underused
#23If you’re looking for a higher-level interface to SAT, SMT, and general constraint solvers, I can recommend MiniZinc: https://www.minizinc.org/index.html
Re: Modern SAT solvers: fast, neat and underused
#24Earlier 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…
... 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!
Re: Modern SAT solvers: fast, neat and underused
#25Earlier quoted context omitted.
At a local group we have weekly meetings where we cook dinner. Two people cook, and two people do the dishes. I used a SAT solver (z3) to find optimal schedules given that people want the tasks to be distributed fairly, but also given other secondary criteria such as mixing up which pairs cook together, prevent being assigned a task two weeks in a row or getting the same task twice in a row, etc.
That's fascinating! I've always wanted to build a similar system for assigning chores around the house based on everyone "bidding" on how much they see the effort of each chore being. In theory, one should be able to come up with an assignment where everyone believes they're doing less than everyone else, by their own metric of work effort. Applying computer science to everyday life is so rare but lovely.
I studied Simplex and related techniques at University, and took https://courses.edx.org/courses/course-v1:MITx+15.053x+3T201... as a refresher.
The course is now closed, but you can probably find something similar as a MOOC.
Re: Modern SAT solvers: fast, neat and underused
#26SAT 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 have used the Z3 solver( https://github.com/Z3Prover/z3 ) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes some variable amount of time to complete and can only be run during specific windows. Given the equipment can only perform P tasks in parallel, what is the optimal configuration of t…
amazing, I tried doing this recently but I guess my modeling was not good enough and it would take hours to find the solution with a couple of dozen variables. Do you have any pointers on how to much these types of problems with a SMT/SAT solver efficiently?
Re: Modern SAT solvers: fast, neat and underused
#27SAT 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 have applied SATs with some success to generative models where sampling methods would not work well, e.g. if you have many soft and hard constraints. Another alternative is to use neural guides.
do you have any pointers on modeling with soft/hard constraints and SAT solvers?
Re: Modern SAT solvers: fast, neat and underused
#28Earlier quoted context omitted.
Cracking product keys for... Uh... Research. You reverse engineer the binary, enter the conditions into an sat solver and boom. But I don't think most keys are implemented this way these days. Also if you want cool, check out uc Santa Barbara's team for the darpa cyber challenge a few years ago for an autonomous hacking system. Their framework, angr, makes use a lot of sat solvers although I didn't quite understand e…
Based on my experience, most key requiring programs use public key crypto and pin their public key in the binary to verify the signature, which is the key.
That hasn't been my experience.
I've seen some that use public key crypto, but mostly they do not because even the smallest secure cryptosystems have signatures on the order of at least 20 bytes (and more conventional choices more like 256-bit ECDSA... 64 bytes)-- which, after conversion to typeable characters, are a bit unwieldy.
Re: Modern SAT solvers: fast, neat and underused
#29This is an interesting read, but I'd be interested in a more large-scale benchmark. Right now it could be possible that the SAT solver is just better optimized for the particular platform, instead of the SAT solver being superior algorithm-wise.
Re: Modern SAT solvers: fast, neat and underused
#30Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem.
Since specialized solvers do thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) that the author mentions in part 1 of the series:
For 17-clue puzzles (which are generally very easy), JCZSolve is 50x as fast as Minisat, and it makes on average ~1.9 decisions per puzzle compared to Minisat's ~3.0. But if you look at the hardest dataset JCZSolve is only 10x as fast as Minisat, and it makes on average ~365 decisions per puzzle compared to Minisat's ~121. I'm not aware of a highly specialized and optimized Solver for 16x16 clue or larger Sudoku, but given this trend my guess is that it would take a lot of effort to write one that's faster than what you get with Minisat for free.
[1] https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE...