Finding all solutions of the Boolean satisfiability problem, if any, via Boolean-equation solving

Abstract EN

Boolean Satisfiability (SAT) is the problem of deciding whether a propositional logic formula can be satisfied given suitable value assignments to the variables of the formula.

This problem is highly intractable to the extent that the most efficient algorithms for solving it require exponential time in the worst case.

Boolean Satisfiability has many applications and emerges frequently in a variety of (occasionally unexpected!) situations.

This fact warrants the availability of a handy tool to tackle small instances of Boolean Satisfiability.

Such a tool is naturally different from existing sophisticated algorithms that handle large and gigantic instances of SAT.

This paper presents a simple introductory exposition of Boolean Satisfiability and provides a method for finding all its solutions, if any, by solving a two-valued Boolean equation.

The method requires several steps including the conversion of a product-of-sums expression to a sum-of-products one, rules of intelligent multiplication, use of the branch-and-bound method and the divide-and-conquer strategy, and finally replacing an ordinary sum of products by a disjoint one.

The paper demonstrates its method, including all its aforementioned steps, via two detailed examples.