2 ms·
The SAT solvers related to Lingeling use kNN to "predict the origin of the benchmark" (I assume to figure out which bucket or set of SAT problems the system was
by zitterbewegung 9y ago
The SAT solvers related to Lingeling use kNN to "predict the origin of the benchmark" (I assume to figure out which bucket or set of SAT problems the system was given and then tune itself to the optimal settings in the bucket).