






















Using Maple, we implement a SAT solver based on the principle of inclusion-exclusion and the Bonferroni inequalities. Using randomly generated input, we investigate the performance of our solver as a function of the number of variables and number of clauses. We also test it against Maple's built-in tautology procedure. Finally, we implement the Lovász local lemma with Maple and discuss its applicability to SAT.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。