SATisfying Solutions to Difficult Problems • Hacker News Board

Re: SATisfying Solutions to Difficult Problems

#51

Post by JonChesterfield » Tue, Oct 28, 2025, 8:44 PM UTC

fulafel wrote: post #44

zero_k wrote: post #37

Earlier quoted context omitted.

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

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?

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.

Re: SATisfying Solutions to Difficult Problems

#52

Post by JonChesterfield » Tue, Oct 28, 2025, 8:46 PM UTC

pfdietz wrote: post #18

roenxi wrote: post #6

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 qui…

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.

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.

Re: SATisfying Solutions to Difficult Problems

#53

Post by js8 » Tue, Oct 28, 2025, 8:53 PM UTC

dooglius wrote: post #50

js8 wrote: post #20

I don't understand why SAT solvers don't use gaussian elimination more. Every SAT problem can be represented as an intersection of linear (XORSAT) and 2SAT clauses, and the linear system can resolve some common contradictions, propagate literals, etc. Also Grobner basis algorithm over polynomials in Z_2 can be used to solve SAT. A SAT problem can be encoded as a set of quadratic polynomials, and if the generated idea…

SAT is NP-complete, and both gaussian elimination and 2SAT are polynomial-time, so this would suggest either you're mistaken or there is some hidden catch here (like the size of one or the other being exponential-sized).

There is no catch - I even describe the reduction in another comment below. You can convert a 3SAT clause to a combination of XORSAT and 2SAT clauses. I am not mistaken, either, I used this reduction many times on practical problems, so I know it works. I encourage you to try it.

Unfortunately, putting the algorithms for XORSAT and 2SAT together is not trivial at all, they are quite different (but Grobner bases over GF(2) seem very promising in that).

But I agree that the fact that both XORSAT and 2SAT have polynomial algorithms is quite a strong indicator that full SAT has a one too. :-) (On the other hand, there is IMHO only very little actual evidence for P!=NP.)

Re: SATisfying Solutions to Difficult Problems

#54

Post by eru » Wed, Oct 29, 2025, 7:03 AM UTC

fulafel wrote: post #44

zero_k wrote: post #37

Earlier quoted context omitted.

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

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?

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.

Re: SATisfying Solutions to Difficult Problems

#55

Post by eru » Wed, Oct 29, 2025, 7:06 AM UTC

fjfaase wrote: post #14

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…

> Sudokus that can be solved with reasoning alone, [...]

Is 'reasoning alone' actually well defined in the context of Sudoku?

Sudoku's are finite, so I can solve all of them with just a lookup table in constant time..

Re: SATisfying Solutions to Difficult Problems

#56

Post by muragekibicho » Wed, Oct 29, 2025, 8:04 AM UTC

eru wrote: post #55

fjfaase wrote: post #14

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…

> Sudokus that can be solved with reasoning alone, [...] Is 'reasoning alone' actually well defined in the context of Sudoku? Sudoku's are finite, so I can solve all of them with just a lookup table in constant time..

I coded the paper Sinkhorn Solves Sudoku. Lol the most bizarre algorithms can solve sudoku. https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku

Re: SATisfying Solutions to Difficult Problems

#57

Post by fjfaase » Wed, Oct 29, 2025, 12:56 PM UTC

muragekibicho wrote: post #56

eru wrote: post #55

Earlier quoted context omitted.

> Sudokus that can be solved with reasoning alone, [...] Is 'reasoning alone' actually well defined in the context of Sudoku? Sudoku's are finite, so I can solve all of them with just a lookup table in constant time..

I coded the paper Sinkhorn Solves Sudoku. Lol the most bizarre algorithms can solve sudoku. https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku

The link https://leetarxiv.substack.com/sinkhorn-solves-sudoku reports 'Page not found'.

Re: SATisfying Solutions to Difficult Problems

#58

Post by muragekibicho » Wed, Oct 29, 2025, 2:02 PM UTC

fjfaase wrote: post #57

muragekibicho wrote: post #56

Earlier quoted context omitted.

I coded the paper Sinkhorn Solves Sudoku. Lol the most bizarre algorithms can solve sudoku. https://github.com/MurageKibicho/Sinkhorn-Solves-Sudoku

The link https://leetarxiv.substack.com/sinkhorn-solves-sudoku reports 'Page not found'.

I've not yet published the writeup. Only the C code is available atm. I solo run a thing called LeetArxiv. It's a successor to Papers with Code since the latter shut down.