Solving satisfiability using inclusion-exclusion

TL;DR

This paper introduces a novel SAT solver based on inclusion-exclusion principles, evaluates its performance against existing methods, and explores the application of the Lovász local lemma in SAT solving.

Contribution

It presents a new SAT solving approach using inclusion-exclusion and Bonferroni inequalities, and extends the analysis with the Lovász local lemma implementation in Maple.

Findings

The inclusion-exclusion based solver performs competitively on random inputs.

The solver's performance varies with the number of variables and clauses.

The Lovász local lemma has potential applicability to SAT problems.

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.