alt Hacker NewsI 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
Replies
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.
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.
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!).