Autoresearch for SAT Solvers
github.com
Autoresearch for SAT Solvers
1–10 of 38 posts
Re: Autoresearch for SAT Solvers
#2It 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.
Re: Autoresearch for SAT Solvers
#3It 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.
Or for that matter even from later versions of the same solvers that were in its training data!
Re: Autoresearch for SAT Solvers
#4It 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.
Or for that matter even from later versions of the same solvers that were in its training data!
True. I’d be curious whether a combination of matching comp/training cutoff and censoring web searches could yield a more precise evaluation.
Re: Autoresearch for SAT Solvers
#5Prof. Cunxi Yu and his students at UMD is working on this exact topic and published a paper on agents for improving SAT solvers [1].
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.
[1] "Autonomous Code Evolution Meets NP-Completeness", https://arxiv.org/abs/2509.07367
Re: Autoresearch for SAT Solvers
#6What counts as “our cost”? How long it takes to find the MaxSAT?
Re: Autoresearch for SAT Solvers
#7It 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.
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.
Re: Autoresearch for SAT Solvers
#8Prof. Cunxi Yu and his students at UMD is working on this exact topic and published a paper on agents for improving SAT solvers [1]. 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. [1] "Autonomous Code Evolution Meets NP-Completeness", https://arxiv.or…
nice. EDA indeed one of the top applications of SAT
Re: Autoresearch for SAT Solvers
#9[dead]
Re: Autoresearch for SAT Solvers
#10It 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.
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.
Funnily, this was precisely the question I had after posting this (and the topic of an LLM disagreement discussed in another thread). Turns out not, but sibling comment is another confounding factor.