A Satisfiability algorithm based on Simple Spinors of the Clifford algebra of $\mathbb{R}^{n,n}$
Marco Budinich
TL;DR
This work reinterprets Boolean SAT within the Clifford algebra ${\cal C}\ell(\mathbb{R}^{n,n})$ by embedding Boolean algebra into idempotents and exploiting simple spinors. It develops both a discrete, algebraic encoding of SAT and a continuous, spinor-based framework via the orthogonal group ${\rm O}(n)$, yielding a polynomial-time unsatisfiability test grounded in geometric properties of null subspaces and spinor supports. The key contributions are (i) constructing a robust Boolean-algebra within Clifford algebra, (ii) formulating SAT in ${\cal C}\ell(\mathbb{R}^{n,n})$ and in ${\rm O}(n)$, and (iii) proposing a spinor-based unsatisfiability test that reduces to checking coverage by clause-induced isometries, with a concrete algorithm outlined for practical use. The approach provides a novel algebraic and geometric lens on SAT, potentially enabling noncombinatorial certificates of unsatisfiability and bridging SAT with spinor geometry and matrix representations of orthogonal groups.
Abstract
We refine the formulation of the Boolean satisfiability problem with $n$ Boolean variables in Clifford algebra ${\cal C}\ell(\mathbb{R}^{n,n})$ [3] and exploit this continuous setting to design a new unsatisfiability test. This algorithm is not combinatorial and proves unsatisfiability in polynomial time.