Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning,
"Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses"
: Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Serie Lecture Notes in Computer Science (LNCS), Vol. 8561, Springer, Seite(n) 302-316, 2014
Original Titel:
Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14)
Original Kurzfassung:
Stochastic Local Search (SLS) solvers are considered one of
the best solving technique for randomly generated problems and more
recently also have shown great promise for several types of hard combinatorial
problems. Within this work, we provide a thorough analysis of
different implementation variants of SLS solvers on random and on hard
combinatorial problems. By analyzing existing SLS implementations, we
are able to discover new improvements inspired by CDCL solvers, which
can speed up the search of all types of SLS solvers. Further, our analysis
reveals that the multilevel break values of variables can be easily
computed and used within the decision heuristic. By augmenting the
probSAT solver with the new heuristic, we are able to reach new stateof-
the-art performance on several types of SAT problems, especially on
those with long clauses. We further provide a detailed analysis of the
clause selection policy used in focused search SLS solvers.
Forschungs-