Satisfiability in Big Boolean Algebras via Boolean-Equation Solving

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 ݃(ࢄ (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 {݃(ࢄ = (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 ݃(ࢄ .(Though the method produces non-compact expressions, it is
much quicker in generating particular solutions. The two methods are demonstrated via two detailed examples.