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