- Beyond NP
https://www.cs.cmu.edu/~bryant/pubdir/fmcad22.pdf tbuddy a proof generating sat solver buddy cudd
https://arxiv.org/abs/2211.06818 CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams
See also berkely abc. AIG and inverter graphs. (RO)BDD are canonical. AIG aren’t
At most one constraints (AMO) Quadratic encoding. not x1 \/ not x2 \/ x3 /\ the other combos logarithmic encoding. y is bitvector of which one is selected. heule encoding
Tseitsin - encode subformulas into a variable
Scalable SAT in the cloud Mallob 2022 HordeSat: A Massively Parallel Portfolio SAT Solver 2015 Cube and Conquer
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 np https://beyondnp.org/ hmm. This website is dead?
beyond SAT quantified boolean. Combining SAT and comuter aogebra model counting
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