TY - GEN
T1 - Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses
AU - Balint, Adrian
AU - Biere, Armin
AU - Fröhlich, Andreas
AU - Schöning, Uwe
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84958538344
U2 - 10.1007/978-3-319-09284-3_23
DO - 10.1007/978-3-319-09284-3_23
M3 - Conference proceedings
VL - 8561
T3 - Lecture Notes in Computer Science (LNCS)
SP - 302
EP - 316
BT - Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14)
PB - Springer
ER -