Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Modern SAT solvers: fast, neat and underused

codingnest.com

Post reply on HN
Print view View original

11–20 of 46 posts

Re: Modern SAT solvers: fast, neat and underused

#11

Post by nextos »

ladberg wrote: post #2

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

Re: Modern SAT solvers: fast, neat and underused

#13

Post by mochomocha »

vasili111 wrote: post #12

Can you please share your personal experience of using SAT solver with real world problem?

Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)

Re: Modern SAT solvers: fast, neat and underused

#14

Post by ackbar03 »

vasili111 wrote: post #12

Can you please share your personal experience of using SAT solver with real world problem?

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 everything when I read their technical docs

Re: Modern SAT solvers: fast, neat and underused

#15

Post by KboPAacDA3 »

ladberg wrote: post #2

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

Re: Modern SAT solvers: fast, neat and underused

#16

Post by foxes »

The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As in you can ask for the input of a function to make your program true.

I imagine all sorts of things can be done like this, and the sat solver is useful for verifying correctness.

Re: Modern SAT solvers: fast, neat and underused

#17

Post by silly_giraffe »

ladberg wrote: post #2

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 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 tasks (~500k) that will allow us to complete the most jobs?

The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.

Re: Modern SAT solvers: fast, neat and underused

#18

Post by nurettin »

wenc wrote: post #10
nurettin wrote: post #5

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…

What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments.

On the other hand, military and hospital applications won't show that weakness.

Re: Modern SAT solvers: fast, neat and underused

#19

Post by wenc »

nurettin wrote: post #18
wenc wrote: post #10

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…

What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments. On the other hand, military and hospital applications won't show that weakness.

Human capriciousness is indeed hard to model, so one solution is not do it. In timetabling applications, the algorithm provides a level of impartiality so even if some constituents don't get what they want, you can always blame the algorithm -- "it tried, but it had to satisfy other constraints".

This removes some (but not all) of the politics behind timetabling. Influential persons may still try to wield their political power to bend the algorithm toward favoring them (e.g. in algorithmic terms, this could mean boosting their weight from 0.5 to 0.8 to beat out competition) but even in this compromised state, optimal timetabling is still better than doing it manually -- the optimization algorithm will at least try to maximize remaining preferences within the remainder degrees-of-freedom.

Timetabling is an inherently political process anywhere (if one has ever done timetable for high school teachers....), but optimization algorithms do bring a level of impartiality to the process. Also, if folks aren't explicit about their preferences, or change their minds, it's no fault of the algorithm.

Re: Modern SAT solvers: fast, neat and underused

#20

Post by xfer »

ackbar03 wrote: post #14
vasili111 wrote: post #12

Can you please share your personal experience of using SAT solver with real world problem?

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.
Post reply on HN