[dead]
Autoresearch for SAT Solvers
31–38 of 38 posts
Re: Autoresearch for SAT Solvers
#32I don't understand why autoresearch is presented as a new thing.
It is parameter tuning. We have been doing it for centuries.
Re: Autoresearch for SAT Solvers
#33I don't understand why autoresearch is presented as a new thing. It is parameter tuning. We have been doing it for centuries.
sure. in the limit, everything is parameter tuning. with large enough NP-hard problems, the complexity of the search space is big enough that its infeasible to get to a better state by just tuning params in any reasonable amount of time.
Re: Autoresearch for SAT Solvers
#34One 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. It would be interesting to take the resulting solver and apply it to an unknown data set.
yess. loads of space for further exploration here. there is an attempt to keep things as general as possible in the expert.md file, but hard to mitigate overfitting fully. however, changing the seed will not get you much further with all else in the solver constant. unless you try a number of seed that exponentially scales with the size of the problem
Re: Autoresearch for SAT Solvers
#35[dead]
nice. for which problem?
Re: Autoresearch for SAT Solvers
#36[dead]
have examples?
Re: Autoresearch for SAT Solvers
#37I don't understand why autoresearch is presented as a new thing. It is parameter tuning. We have been doing it for centuries.
sure. in the limit, everything is parameter tuning. with large enough NP-hard problems, the complexity of the search space is big enough that its infeasible to get to a better state by just tuning params in any reasonable amount of time.
I beg to disagree. Integer programming solvers have improved orders of magnitude in the past 20 years. The basic algorithm (branch and bound) is the same.
The big commercial solvers basically are very good at picking up structures and selecting the tuning parameters that work better for specific problem types.
Re: Autoresearch for SAT Solvers
#38Very interesting. For me the key question is whether this kind of agent can generalize to real SAT application domains, not only benchmark instances. In problems like timetabling, encoding choices, auxiliary variables, and branching strategy can matter a lot. If it can help there too, this is a very meaningful direction.