# SAT Solvers

## Encoding

## CDCL

## 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?

Quadrangulation using a SAT solver satsort I’m not sure what this is

AWS automated reasoning frontier mallob-mono Good sat solver enabled “Seshia” tehcnique for smt? https://github.com/awslabs/rust-smt-ir bounds integers and turns to bitvectors + ackermannization

beyond SAT quantified boolean. Combining SAT and comuter aogebra model counting

Soos proof traces for sat solvers FRAT

similiarty metric between solutions model-core in cvc5

gimsatul another armin biere experiment. parallel?

https://twitter.com/ArminBiere/status/1556292768607207425?s=20&t=yqv3psiW3ByDbnVTBLr_GA Kissat is domainting. The parallel and cloud solvers have really interesting things going on. mallob-ki. parkissat-rs is parallel winner