SATisfying Solutions to Difficult Problems • Hacker News Board

Re: SATisfying Solutions to Difficult Problems

#41

Post by taeric » Tue, Oct 28, 2025, 4:51 PM UTC

zero_k wrote: post #37

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…

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…

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

Re: SATisfying Solutions to Difficult Problems

#42

Post by js8 » Tue, Oct 28, 2025, 5:25 PM UTC

zero_k wrote: post #36

sirwhinesalot wrote: post #21

Earlier quoted context omitted.

I have no idea about most of the words you wrote but I'd love to see alternative approaches to SAT solving. CryptoMiniSAT has native support for Gaussian Elimination but it has to put a lot of effort into recovering XORs from the CNF. A different format (XORSAT + 2SAT) plus an efficient algorithm to exchange information from the two sides of the problem would be interesting.

Author of CryptoMiniSat here :) XOR+CNF is indeed supported by CryptoMiniSat. Which is cool, but if you _really_ think about it, the resolution operator over these two are gonna give you multivariate polynomials over GF(2). So resolution is poor in CryptoMiniSat, because it only encodes one of the constraints that this polynomial implies (i.e. one that can be encoded in a single disjunctive clause). And if you wanna…

Thanks for the links to those people. The GF(2) simplifies Grobner bases calculations a lot, IMHO, but I don't have much experience with them either. I am just curious, because to me it now seems to be an obvious way to go. I mean, the fact that we can represent any SAT problem as an intersection of 2SAT and XORSAT problems indicates, there must be some generalization of the both polynomial algorithms. And it seems to me this generalization is somehow related to Grobner bases methods.

I have only very quickly skimmed it, but I wouldn't be surprised if the theorem D.21 in Kaufman's thesis (https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufma...) turned out to be true for all the unsatisfiability PAC proofs, not just the circuits she is looking at. (As I commented below. If you're proving contradiction, looking for element 1 in the ideal using Grobner basis, then it seems somewhat unreasonable to require degree of basis polynomials larger than 3, if you start from all polynomials with degree less or equal than 2. If you look what e.g. 2SAT algorithm is doing algebraically, it only needs degree 3 polynomials as well, although the monomial of degree 3 is immediately eliminated. So if the Grobner basis algorithm needs to build large degree polynomials, because no small degree will help you, it's likely your system is already satisfiable. Would really like to see a counterexample.)

Re: SATisfying Solutions to Difficult Problems

#43

Post by dualogy » Tue, Oct 28, 2025, 5:51 PM UTC

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…

> 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 =)

Re: SATisfying Solutions to Difficult Problems

#44

Post by fulafel » Tue, Oct 28, 2025, 6:01 PM UTC

zero_k wrote: post #37

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…

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?

Re: SATisfying Solutions to Difficult Problems

#45

Post by dekhn » Tue, Oct 28, 2025, 6:11 PM UTC

dualogy wrote: post #43

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…

> 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 =)

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

Re: SATisfying Solutions to Difficult Problems

#46

Post by BigTTYGothGF » Tue, Oct 28, 2025, 6:47 PM UTC

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…

> I don't understand how we can get high degree polynomials when running Grobner basis algorithm

From the syzygies, surely?

Re: SATisfying Solutions to Difficult Problems

#47

Post by FreakLegion » Tue, Oct 28, 2025, 6:54 PM UTC

sirwhinesalot wrote: post #25

zvr wrote: post #17

Earlier quoted context omitted.

Many thanks to you and the parent comment for providing names to search when looking for implementations. A basic question, before searching these: are they "input compatible"? I mean, can a problem be formulated once and then be solved by a variety of solvers? Or does each one of them use its own input language?

For MILP there isn't one single standard, but multiple competing solutions. Nearly every solver supports the MPS format, but that's a really old format straight from the era of punchcards, it sucks. Many solvers support the nl format, which is a low level format spat out by the AMPL tool (commercial software for mathematical modeling). Many solvers support the CPLEX lp format, which is a nice human readable and writa…

This is a good list --- would also add Pyomo. There's plenty of nuance to algebraic modeling languages like Pyomo and JuMP, but at base you're just writing mathematical expressions in Python for Pyomo (or in Julia for JuMP) to parse and transform into the target format. E.g. taking the objective from the Weapon Target Assignment problem (https://en.wikipedia.org/wiki/Weapon_target_assignment_probl...):

    def objective(model: WtaModel) -> SumExpression:
        return sum(
            model.target_values[t_j]
            * prod(
                model.survival_rates[w_i][t_j]
                ** model.target_selected[w_i, t_j]
                for w_i in model.weapon_types
            )
            for t_j in model.targets
        )

Re: SATisfying Solutions to Difficult Problems

#48

Post by js8 » Tue, Oct 28, 2025, 7:24 PM UTC

BigTTYGothGF wrote: post #46

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…

> I don't understand how we can get high degree polynomials when running Grobner basis algorithm From the syzygies, surely?

Surely. Maybe you can give me a counterexample. Let's just consider GF(2). Give me a set of generators with polynomials of degree See my problem? Somehow, I feel these syzygies need to be constructed from the degree 2 polynomials (the initial set), but then we can probably only work with the polynomials of the low degree instead, from which those syzygies are constructed.

To me, this is a very interesting question. Because if we can find the Grobner basis (even for just those ideals that coincide with the whole ring) in GF(2) in a way that we only need to construct polynomials of bounded degree, then there is a polynomial algorithm for SAT. Since most people believe there isn't such algorithm, I would really like to see a counterexample to this situation.

Re: SATisfying Solutions to Difficult Problems

#49

Post by FreakLegion » Tue, Oct 28, 2025, 7:30 PM UTC

sirwhinesalot wrote: post #12

FreakLegion wrote: post #9

Earlier quoted context omitted.

SCIP going Apache definitely improved the landscape, but Couenne (global MINLP), Bonmin (local MINLP), and IPOPT (local NLP, but e.g. [1] gets you MINLP) are solid and have been around for a long time. And anecdotally, I've seen a lot more issues with SCIP (presolvers and tolerances, mostly) than with other solvers. Still it's replaced Couenne in my toolbox, and Minotaur has replaced Bonmin, but IPOPT remains king of…

Didn't know about Randomized rounding. Is there any solver with built-in support for that? To turn a strong NLP solver into a fast but approximate MINLP solver?

Not necessarily randomized rounding in particular, but many solvers use rounding methods internally e.g. as part of a feasibility pump. Minotaur and SCIP definitely do this.

Re: SATisfying Solutions to Difficult Problems

#50

Post by dooglius » Tue, Oct 28, 2025, 8:31 PM UTC

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