Projective cofactor decompositions of Boolean functions and the satisfiability problem

TL;DR

This paper introduces a new recursive algorithm for SAT that uses projective cofactors to decompose the problem into independent sub-problems, enabling parallel solution computation.

Contribution

The paper presents a novel SAT algorithm based on projective cofactors, independent of previous orthogonal expansion methods, allowing parallelization and efficient solution enumeration.

Findings

Recursive decomposition into independent sub-problems

Parallel algorithm for SAT decision and solution enumeration

Effective handling of CNF formulas using projective cofactors

Abstract

Given a CNF formula $F$, we present a new algorithm for deciding the satisfiability (SAT) of $F$ and computing all solutions of assignments. The algorithm is based on the concept of \emph{cofactors} known in the literature. This paper is a fallout of the previous work by authors on Boolean satisfiability \cite{sul1, sul2,sude}, however the algorithm is essentially independent of the orthogonal expansion concept over which previous papers were based. The algorithm selects a single concrete cofactor recursively by projecting the search space to the set which satisfies a CNF in the formula. This cofactor is called \emph{projective cofactor}. The advantage of such a computation is that it recursively decomposes the satisfiability problem into independent sub-problems at every selection of a projective cofactor. This leads to a parallel algorithm for deciding satisfiability and computing all solutions of a satisfiable formula.