Power Term Polynomial Algebra for Boolean Logic

TL;DR

This paper introduces power term polynomial algebra, a novel representation for Boolean formulas that unifies CNF and ANF forms, enabling efficient manipulation without exponential blowup.

Contribution

It formalizes a new algebraic language for Boolean logic that directly encodes CNF clauses and supports algebraic operations, bridging the gap between clause-based and algebraic reasoning.

Findings

Compact canonical representations for disjunctive clauses

Supports local rewriting rules for power terms

Enables algebraic manipulation of Boolean formulas without expansion

Abstract

We introduce power term polynomial algebra, a representation language for Boolean formulae designed to bridge conjunctive normal form (CNF) and algebraic normal form (ANF). The language is motivated by the tiling mismatch between these representations: direct CNF<->ANF conversion may cause exponential blowup unless formulas are decomposed into smaller fragments, typically through auxiliary variables and side constraints. In contrast, our framework addresses this mismatch within the representation itself, compactly encoding structured families of monomials while representing CNF clauses directly, thereby avoiding auxiliary variables and constraints at the abstraction level. We formalize the language through power terms and power term polynomials, define their semantics, and show that they admit algebraic operations corresponding to Boolean polynomial addition and multiplication. We prove several key properties of the language: disjunctive clauses admit compact canonical representations; power terms support local shortening and expansion rewrite rules; and products of atomic terms can be systematically rewritten within the language. Together, these results yield a symbolic calculus that enables direct manipulation of formulas without expanding them into ordinary ANF. The resulting framework provides a new intermediate representation and rewriting calculus that bridges clause-based and algebraic reasoning and suggests new directions for structure-aware CNF<->ANF conversion and hybrid reasoning methods.