Power Term Polynomial Algebra for Boolean Logic
Emanuele Sansone, Armando Solar-Lezama

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge
