Autoresearch for SAT Solvers

(github.com)

47 points | by chaisan 2 hours ago

3 comments

  • stefanpie 31 minutes ago
    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].

    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

  • ericpauley 44 minutes ago
    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.
    • jmalicki 40 minutes ago
      Or for that matter even from later versions of the same solvers that were in its training data!
      • ericpauley 39 minutes ago
        True. I’d be curious whether a combination of matching comp/training cutoff and censoring web searches could yield a more precise evaluation.
  • gsnedders 9 minutes ago
    What counts as “our cost”? How long it takes to find the MaxSAT?