2017/12/15 by Anthony Zaleski, Zaleski, Anthony
Computer Science · Mathematics · Psychology · #68R01 #68W40 #Advanced Algebra and Logic #Algorithm #Combinatorics (math.CO) #Computer science #Data Management and Algorithms #Data Structures and Algorithms (cs.DS) #Discrete mathematics #FOS: Computer and information sciences #FOS: Mathematics #Inclusion (mineral) #Lemma (botany) #Logic, Reasoning, and Knowledge #Maple #Mathematics #Programming language #Psychology #Solver #Tautology (logic) #Theoretical computer science #cs.DS #math.CO #msc:68R01 #msc:68W40
paper · pdf · doi:10.48550/arxiv.1712.06587
11 pages, 3 figures, Maple package available on author's site
arxiv created 2017/12/15 · openalex publication_date 2017/12/15 · arxiv updated 2017/12/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.