Hacker News Reader

Comment by NooneAtAll3 | Hacker News Reader

I love SAT solver papers, always interesting to see auxiliary variable techniques, since those aren't really listed anywhere central

here for example, instead of saying {f(x,y,z)==g(x,y,z)}, authors instead make variable group a_w:=(f(x,y,z)=w||g(x,y,z)=w), and then apply "at most 1" to it. Can't be unequal if both functions only can have 1 result in total

this adds an index to iterate over, but separates internal subexpressions of f() and g(), removing 2 indixes (in this problem) and thus dropping whole power of n of clauses

---

what I don't get is that they aren't searching Tarski's problem per se, but for one specific solution to it (one identity that isn't resulting from given). I'd totally look for arithmetic models that violate expectations in other ways than Wilkie

View on HN

Indeed, having a different "exotic identity" that has smaller countermodels would be awesome. Unfortunately, we tried a few alternatives to Wilkies and didn't find smaller countermodels.

Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...

(I'm one of the authors of the paper, thanks for the coment!).

> we tried a few alternatives to Wilkies and didn't find smaller countermodels.

I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives)

---

by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?

---

also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)

> I wish you spent at least a couple words in the paper about that.

That makes sense; it just happened that we tried the other identities after having written and submitted the paper. More importantly, the variants of Wilkie's identity we tried were suggested to us by an expert on the topic; I have just sent an email asking if they are okay with us sharing them, and if so I will post a link here.

> how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?

It was roughly a factor of 8 fewer clauses, and yet over 5 times slower. If you're interested in the design of compact CNF encodings, and their effects on runtime, that's exactly the topic of my PhD thesis, and this proposal might give an initial idea: https://bsubercaseaux.github.io/assets/pdf/proposal.pdf

Naturally, there could be another encoding that has fewer clauses (say, O(n^5) or even O(n^4)) and does perform better in practice. But we didn't come up with one.

> also, have you tried reordering order of operations in symmetry break? how much did it affect the search?

To some extent. It was of moderate impact in terms of the runtime, but presumably the enumeration up to isomorphism would have been harder if we didn't consider the addition variables first. To have some updated numbers, I just ran some experiments with the 3! = 6 permutations of {A, M, E} on n=10.

AME (used in the paper) -> 92.7s AEM -> 110.8s MAE -> 139.4s MEA -> 157.4s EAM -> 297.1s EMA -> 276.8s

Man I wish I understood anything you said, or anything in tfa. Math has to have my personal gold medal for highest desire to learn coupled with total unwillingness to.

in a sense it's about a game. or... maybe it's better to call it a "challenge"

Tarski said "hey, what if we limit ourself only to positive integers? subtraction/division doesn't always work, so let's get rid of it. What can we say about +^? there are some obvious properties, like x+y=y+x for whatever x and y. Is that enough to describe all the equalities?".

Wilkie answered No, and a whole different hunt began - trying to find a set of pseudo "numbers" with pseudo "+^", that would have the same obvious properties, but not the non-obvious one

and SAT-solving is essentially asking computer to find things by describing what they are not - "1+2 is not invalid and can't be 2 different values", "1+(1+1) must not differ from (1+1)+1". A lot of such properties are easily expressible as "not the opposite" - but devil's in the details and some choices of opposites are faster for computer than others. Also symmetries are evil :)

They use the properties of Wilkie's counterexample to restrict the search space. So you can't just pick arbitrary identities that hold over the positive integers and repeat the process until you've found a smaller model.

Reply on news.ycombinator.com