Prof. Cunxi Yu and his students at UMD is working on this exact topic and published a paper on agents for improving SAT solvers [1].<p>I believe they are extending this idea to EDA / chip design tools and algorithms which are also computationally challenging to solve. They have an accepted paper on this for logic synthesis which will come out soon.<p>[1] "Autonomous Code Evolution Meets NP-Completeness", <a href="https://arxiv.org/abs/2509.07367" rel="nofollow">https://arxiv.org/abs/2509.07367</a>
It should be noted that MaxSAT 2024 did not include z3, as with many competitions. It’s possible (I’d argue likely) that the agent picked up on techniques from Z3 or some other non-competing solver, rather than actually discovering some novel approach.
Z3 is capable (it’s an SMT solver, not just SAT), but it’s not very fast at boolean satifiability and not at all competitive with modern SOTA SAT solvers. Try comparing it to Chaff or Glucose e.g.
Or for that matter even from later versions of the same solvers that were in its training data!
Is z3 competitive in SAT competitions? My impression was that it is popular due to the theories, the python API, and the level of support from MSR.
One problem here is it's very easy to overtune to a past problem set -- even accidentally. You can often significantly improve performance just by changing your random number generator seed until you happen to pick the right assignment for the first few variables of some of the harder problems.<p>It would be interesting to take the resulting solver and apply it to an unknown data set.
Not as many changes to the files under library as I expected to see. Most changes seemed to be under a single ‘add stuff’ commit. If some of the solvers are randomised, then repeatedly running and recording best solution found will continually improve over time and give the illusion of the agent making algorithmic advancements, won’t it?
fine tuning a small model usually beats prompting a large one for specific tasks imo
What counts as “our cost”? How long it takes to find the MaxSAT?
sounds like AlphaDev [1] might be a better approach for a problem like this.<p>[1] <a href="https://github.com/google-deepmind/alphadev" rel="nofollow">https://github.com/google-deepmind/alphadev</a>
Would me be nice to try this on lcg (CP-SAT) solvers
we've been running something similar in prod. latency is the real bottleneck not accuracy
anyone else finding that agent architectures are way more expensive than expected?
interesting results but the eval methodology seems a bit optimistic