• Verilog

BDD tbuddy a proof generating sat solver buddy cudd


pgbdd pgpbs 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

Graph constraints

Tseitsin - encode subformulas into a variable


pysat encoding into sat



preprcoessing in sat, maxsat, qbf


Parallel SAT

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: matrix multiplication, problems with high symettry, graph coloring, pythoagorean triple problem

Seems very reasonable for max sat too?

Beyond NP

Model Counting CPOG Knowledge Compiler Certifier

beyond np hmm. This website is dead?

knowledge compilation


Maxsat Combining Clause Learning and Branch and Bound for MaxSAT maxcdcl


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

sat solver for factorio

similiarty metric between solutions model-core in cvc5

gimsatul another armin biere experiment. parallel? Kissat is domainting. The parallel and cloud solvers have really interesting things going on. mallob-ki. parkissat-rs is parallel winner

The silent revolution of sat


IPASIR-UP: User Propagators for CDCL

On Solving Word Equations Using SAT