Satisfiability in big Boolean algebras via Boolean-equation solving

Abstract EN

This paper studies Satisfiability (SAT) in finite atomic Boolean algebras larger than the two-valued one B2, which are named big Boolean algebras.

Unlike the formula g(X) in the SAT problem over B2, which is either satisfiable or unsatisfiable, this formula for the SAT problem over a big Boolean algebra could be unconditionally satisfiable, conditionally satisfiable, or unsatisfiable depending on the nature of the consistency condition of the Boolean equation {g(X)=1}, since this condition could be an identity, a genuine equation, or a contradiction.

The paper handles this latter SAT problem by using a conventional method and a novel one for deriving parametric general solutions, and subsequently utilizing expansion trees for generating all particular solutions of the aforementioned Boolean equation.

Each of these two methods could be cast in pure algebraic form, but becomes much easier to visualize and comprehend when presented via the natural map of a big Boolean algebra, which (for historical reasons) is called the variable-entered Karnaugh map (VEKM).

In the classical method, the number of parameters used is minimized and compact solutions are obtained.

However, the parameters belong to the underlying big Boolean algebra.

By contrast, the novel method does not attempt to minimize the number of parameters used, as it uses independent parameters belonging to the two-valued Boolean algebra B2 for each asserted atom in the Boole-Shannon expansion of the formula g(X).

Though the method produces non-compact expressions, it is much quicker in generating particular solutions.

The two methods are demonstrated via two detailed examples.