|
|
|
|
|
by lou1306
785 days ago
|
|
SAT appears to be rather impervious to statistical methods because it is very non-linear and non-local (besides, of course, being NP-complete). Flip one single literal anywhere and poof!, your formula mght go from SAT to UNSAT, or vice versa, or you might enable a ton of simplifications, etc. So it might be very hard to train a network on such a riotous state space. 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. |
|
But people hope that some subclass of "real-life" instances of one of these optimization problems has enough structure that AI/ML may be able to learn useful heuristics for it. (This is not my field. This is just my take-away from reading some AI/ML-for-CO papers.)