sounds like AlphaDev [1] might be a better approach for a problem like this.
Autoresearch for SAT Solvers
11–20 of 38 posts
Re: Autoresearch for SAT Solvers
#12[dead]
its just comparing the cost of the best solution found to the best known cost we had before. O(N). why optimistic?
Re: Autoresearch for SAT Solvers
#13Earlier quoted context omitted.
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.
as its from 2024 (MaxSAT was not held in 2025), its quite likely all the solvers are in the training data. so the interesting part here is the instances for which we actually got better costs that what is currently known (in the best-cost.csv) file.
Re: Autoresearch for SAT Solvers
#14What counts as “our cost”? How long it takes to find the MaxSAT?
the sum of the weights of the unsatistied clauses. we want to reduce this number
Re: Autoresearch for SAT Solvers
#15[dead]
Re: Autoresearch for SAT Solvers
#16Not 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?
Re: Autoresearch for SAT Solvers
#17Would me be nice to try this on lcg (CP-SAT) solvers
Re: Autoresearch for SAT Solvers
#18Not 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?
yeh. ofc. but on any problem larger than 40 variables, the gains from random restarts or initializations will quickly plateau
Re: Autoresearch for SAT Solvers
#19Not 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?
yeh. ofc. but on any problem larger than 40 variables, the gains from random restarts or initializations will quickly plateau
and it would take an algo change to the solver to jump to the next local optimum
Re: Autoresearch for SAT Solvers
#20sounds like AlphaDev [1] might be a better approach for a problem like this. [1] https://github.com/google-deepmind/alphadev
somewhat