Inverse Intersections for Boolean Satisfiability Problems
Paul W. Homer
TL;DR
This work introduces a matrix representation $R_M$ for CNF/SAT problems, where variables form rows and clauses form columns, with entries $T$, $F$, or $U$. It defines a binary-tree, path-based interpretation that yields membership sets $R_S$ and, via reversal and bit-flipping, the answer sets $R_A$, providing a formal mapping between clause structure and satisfying assignments. The core contribution is the inverse-intersection framework: each clause has an inverse $I_i$ capturing the paths not covered by that clause, and the global solution set is the intersection $R_A = I_1 \cap I_2 \cap \dots \cap I_C$, enabling pruning through structured intersections. While the method demonstrates exponential worst-case complexity, it operates on polynomial-sized representations and leverages disjoint inverses to control fragmentation, offering a novel, path-aware perspective on solving $k$-SAT problems. The approach potentially informs alternative SAT-solving strategies by reframing clause interactions as inverse-path intersections within a hierarchical tree representation.
Abstract
Boolean Satisfiability (SAT) problems are expressed as mathematical formulas. This paper presents a matrix representation for these SAT problems. It shows how to use this matrix representation to get the full set of valid satisfying variable assignments. It proves that this is the set of answers for the given problem and is exponential in size relative to the matrix. It presents a simple algorithm that utilizes the inverse of each clause to find an intersection for the matrix. This gives a satisfying variable assignment.