Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Power Term Polynomial Algebra for Boolean Logic

Emanuele Sansone, Armando Solar-Lezama

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.

Power Term Polynomial Algebra for Boolean Logic

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.
Paper Structure (12 sections, 9 theorems, 24 equations, 3 figures)

This paper contains 12 sections, 9 theorems, 24 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Conversions and the Tiling Mismatch
  4. Power Term Polynomial Algebra
  5. Power Terms
  6. Power Term Polynomials
  7. Properties of Power Term Polynomials
  8. Power Term Polynomial Algebra
  9. Power Term Polynomial Calculus
  10. Conclusion and Future Work
  11. Proof of \ref{['shorten_expand']}
  12. Proof of \ref{['maintheorem']}

Key Result

Proposition 14

Minimal power term polynomials are not canonical with respect to Boolean polynomials.

Figures (3)

  • Figure 1: Abstraction steps illustrating the transformation of Boolean polynomials into power terms. The symbol $\times$ indicates that the corresponding set of sets representation cannot be expressed as a single power set.
  • Figure 2: Syntax and (denotational) semantics of the abstraction language based on power term polynomials. A power term polynomial generated by this grammar is well formed if every power term $S.\mathbf{P}_U$ satisfies the conditions of Definition \ref{['power_term']}. The operators $\uplus$ and $\odot$ satisfy the algebraic laws given in their respective definitions and are interpreted as addition and multiplication over $\mathbb{F}_2$, respectively.
  • Figure 3: Multiplication rules for any two power terms. Conditions are checked according to the ordering given by the corresponding number. The rules always produce power term polynomials of size no greater than 3. Better visualization by zooming in the figure. A larger version is provided in the Appendix.

Theorems & Definitions (28)

  • Example 1
  • Example 2
  • Example 3
  • Remark 4
  • Example 5
  • Definition 6: Power Set
  • Example 7
  • Definition 8: Power Term
  • Example 9
  • Example 10
  • ...and 18 more