2020-12-16

SAT
k k + 1
辿
Prolog

SAT
SAT
DPLL, CDCL DPLL CDCL CDCL
>survey inspired decimation
SAT
SAT competition CDCL
CDCL
CDCL
SAT
NP
P NP
SAT solver
solver sat competition
SAT solver SAT solver 2
DPLL 4
breakthrough heuristics
4
implication graph
DPLL Unit Propagation,
backtrack
implication graph
CDCL implication graph backtrack
implication graph
conflict
decision literal
conflict

hr