Solving satisfiability using inclusion-exclusion
Data Structures and Algorithms
2017-12-20 v1 Combinatorics
Abstract
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\'asz local lemma with Maple and discuss its applicability to SAT.
Keywords
Cite
@article{arxiv.1712.06587,
title = {Solving satisfiability using inclusion-exclusion},
author = {Anthony Zaleski},
journal= {arXiv preprint arXiv:1712.06587},
year = {2017}
}
Comments
11 pages, 3 figures, Maple package available on author's site