|
|
|
|
|
by electricships
778 days ago
|
|
After AlphaZero, people tried to train various combinatorial solvers IIRC, they were unable to exceed Sota of SAT solvers (which admittedly are the results of decades of research) maybe we just needed bigger networks, or transformers, or just more training compute |
|
Additionally, in practice SAT solvers are also supposed to provide witnesses (i.e., a satisfying assignment or an unsatisfiability core) to back their verdicts, and that may be an ever taller order for ML.