[roenxi]

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

[zero_k]

SAT solvers are used _everywhere_. Your local public transport is likely scheduled with it. International trains are scheduled with it. Industrial automation is scheduled with it. Your parcel is likely not only scheduled with it, but even its placement on the ship is likely optimised with it. Hell, it's even used in the deep depths of cryptocurrencies, where the most optimal block composition is computed with it. Even your friendly local nuclear reactor may have had its failure probability computed with (a variation of) it. In other words, it's being used to make your life cheaper/better/safer/easier. Google a bit around, open your eyes Neo ;)

PS: Yes, I develop a propositional SAT solver that used to be SOTA [1]. I nowadays develop a propositional model counter (for computing probabilities), that is currently SOTA [2]

[1] https://github.com/msoos/cryptominisat/ [2] https://github.com/meelgroup/ganak/

[taeric]

I confess I would expect a lot of those would be linear programming more than sat? Mixed integer would not surprise me.

[fulafel]

Are there open source examples of usage for real world problems, for example train scheduling or something else than software engineering practicioners might find relatable?

[JonChesterfield]

Register allocation, instruction selection and instruction scheduling can, with a degree of bloodyminded patience, all be solved with boolean SAT. That's a compiler backend.

I like the higher level CSP more as an interface but those are _probably_ best solved by compilation to SAT. SMT also worth a look.

[eru]

When I used to work at Deutsche Bahn, the German railway operator, in the mid 2000s as a research student, we were using Mixed Integer Linear Programming.

[sirwhinesalot]

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.

[emil-lp]

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

[roenxi]

At doing what, though? Why are they solving the SAT problem?

[emil-lp]

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.

[tannhaeuser]

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.

[maweki]

Incremental automatic grounding to SAT works fine for ASP.

[pxx]

"All" isn't right.

You can only encode decision problems in NP into a SAT instance of polynomially-balanced size. Sure, that's a lot of things, but there are things provably not in this set.

[egl2020]

"SAT solvers only really seem to be good at Sudoku": if you use conda or uv, you've used an SAT solver.

[pfdietz]

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.

[JonChesterfield]

My experience is they respond yes/no very quickly for lots of problems, but as the problem approaches "probably narrowly solvable" the runtime goes exponential.

[taeric]

I'm curious if you have examples of problems you don't think they are good at solving? Agreed that they are not a panacea of solving problems, but if you are able to somewhat naturally reduce your problem to a SAT statement, they are silly tough to beat.

[dualogy]

> 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

"MiniZinc" is the name of the Pythonic-ish-like syntax targeting (ie on-the-fly translating to) numerous different solvers (somewhere around half-a-dozen to a dozen or so, don't recall exactly =)

[dekhn]

I had never used SAT before (was familiar with the concept) and recently wanted to avoid thinking, so I asked gemini (after a few test prompts):

"""Create a MiniZinc script to find the optimal E12-series resistor values for the base ($R_B$) and collector ($R_C$) of a PN2222A transistor switch.

Specifications:

Collector Voltage Supply ($V_{CC}$): 12V DC

Base (Input) Voltage ($V_{IN}$): 3.3V DC

Target Collector Current ($I_C$): Maximize, but do not exceed, 1W (1 watt).

The script must correctly model the circuit to ensure the transistor is in saturation and must execute without Gecode solver errors like 'Float::linear: Number out of limits"""

After a few more try-paste exception loops, that generated a lovely and readable MiniZinc script with variables I can adjust for other circuits. It was exciting to see that basically every constraint problem I learned in school ("at what angle should you swim across the river..." is just a matter of encoding the problem and running a solver (I still think people should learn the basics of constraint problems, but after a certain point the problems are just tricky enough that it makes more sense to teach people how solvers work, and how to encode problems for them...")