Stochastic local search solvers
Simple and sometimes good. DDFW Some examples: http://ubcsat.dtompkins.com/ http://fmv.jku.at/yalsat/ https://github.com/adrianopolus/probSAT matrix multiplication, problems with high symettry, graph coloring, pythoagorean triple problem
Seems very reasonable for max sat too?
beyond SAT quantified boolean. Combining SAT and comuter aogebra model counting
similiarty metric between solutions model-core in cvc5