基数约束SAT的精确求解器[!tldr]文章链接 From Clauses to Klauses [!abstract]Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form.