4 ms·
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 gener
by hirsin 6y ago
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.
- maweki 6y agoIf 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.