A fleet of computers helps settle a 90-year-old math problem

Re:A fleet of computers helps settle a 90-year-old math problem by hirsin on Thursday August 27, 2020 @02:59AM (#24290812)

I brushed up against SAT solvers in school, but never quite got a grasp on them. The "proof" at the end is 200 GB - is that size related to SAT solvers in general, this particular problem, the dimensionality here? A billion-sized search space giving a 1.6 trillion bit proof sounds awfully exhaustive to me, but I also can't imagine what such a large proof would even be about.

[ Parent | on HN ]

Re:A fleet of computers helps settle a 90-year-old math problem by maweki on Thursday August 27, 2020 @06:00AM (#24291932)

If you're talking about boolean satisfiability, all you have as "memory locations" are bits and you describe their relationships. I guess the result you want is "unsat".

Say you want location 1 not equal location 2, then you have

(1 or 2) and (not 1 and not 2) in the expected normal form. This blows up fast if multiple variables are involved. There are tricks like Tseitin transformation that can reduce the size of the clauses but introduces additional variables.

Also, if you want to use 8-bit-numbers, you'd need 8 variables each. Addition would need more clauses.

[ Parent | on HN ]