An algorithm for Boolean satisfiability based on generalized orthonormal expansion

TL;DR

This paper introduces an algorithm based on generalized orthonormal expansion to decide the consistency of Boolean systems and find all solutions, extending classical methods like DPLL for CNF formulas.

Contribution

It develops a novel algorithm utilizing ON expansion for arbitrary Boolean functions, enabling solution enumeration without resolution, and generalizes the DPLL algorithm for CNF formulas.

Findings

Algorithm effectively determines Boolean system satisfiability.

Extension of DPLL algorithm for multi-variable splitting.

Provides a unified framework for Boolean solution characterization.

Abstract

This paper proposes an algorithm for deciding consistency of systems of Boolean equations in several variables with co-efficients in the two element Boolean algebra $B_{0}=\{0,1\}$ and find all satisfying assignments. The algorithm is based on the application of a well known generalized Boole-Shannon orthonormal (ON) expansion of Boolean functions. A necessary and sufficient consistency condition for a special class of functions was developed in \cite{sule} using such an expansion. Paper \cite{sule} develops a condition for consistency of the equation $f(X)=0$ for the special classes of Boolean functions 1) $f$ in $B(\Phi(X))$ for an ON set $\Phi$ of Boolean functions in $X$ over a general Boolean algebra $B$ and 2) $f$ in $B(X_{2})(\Phi(X_{1}))$. The present paper addresses the problem of obtaining the consistency conditions for arbitrary Boolean functions in $B_{0}(X)$. Next, the consistency for a single equation is shown equivalent to another system of Boolean equations which involves the ON functions and characterizes all solutions. This result is then extended for Boolean systems in several variables over the algebra $B_{0}=\{0,1\}$ which does not convert the system into a single equation. This condition leads to the algorithm for computing all solutions of the Boolean system without using analogous resolution and determine satisfiability. For special systems defined by CNF formulas this algorithm results into an extension of the DPLL algorithm in which the \emph{splitting rule} is generalized to several variables in terms of ON terms in the sense that splitting of CNF set in a single variable $x$ is equivalent to ON terms $x,x'$.