Power Term Polynomial Algebra for Boolean Logic

Emanuele Sansone; Armando Solar-Lezama

cs.LOMar 14, 2026

Power Term Polynomial Algebra for Boolean Logic

Authors: Emanuele Sansone, Armando Solar-Lezama

Organizations: CSAIL, MIT, USA · ESAT, KU Leuven, Belgium

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.

Figures & tables

Boolean Poly.		Set of Sets		Power Set		Power Term
$x_{1}$	$\rightarrow$	$\{\{x_{1}\}\}$	$\rightarrow$	$\mathbf{P}_{1}$	$\rightarrow$	$S_{1}.\mathbf{P}_{\emptyset}$
$x_{1}x_{2}$	$\rightarrow$	$\{\{x_{1},x_{2}\}\}$	$\rightarrow$	$\times$	$\rightarrow$	$S_{1,2}.\mathbf{P}_{\emptyset}$
$x_{1}{+}x_{2}{+}x_{1}x_{2}$	$\rightarrow$	$\{\{x_{1}\},\{x_{2}\},\{x_{1},x_{2}\}\}$	$\rightarrow$	$\mathbf{P}_{1,2}$	$\rightarrow$	$S_{\emptyset}.\mathbf{P}_{1,2}$
$x_{3}(x_{1}{+}x_{2}{+}x_{1}x_{2})$	$\rightarrow$	$\{\{x_{1}{,}x_{3}\}{,}\{x_{2}{,}x_{3}\}{,}\{x_{1}{,}x_{2}{,}x_{3}\}\}$	$\rightarrow$	$\times$	$\rightarrow$	$S_{3}.\mathbf{P}_{1,2}$

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.

Syntax			Evaluation
expr	$::=$		$\llbracket$ expr $\rrbracket$	=
		$\texttt{expr}\;\odot\;\texttt{expr}$			$\llbracket$ expr $\rrbracket$ $\cdot$ $\llbracket$ expr $\rrbracket$
		ptpoly			$\llbracket$ ptpoly $\rrbracket$
ptpoly	$::=$		$\llbracket$ ptpoly $\rrbracket$	=
		$\texttt{ptpoly}\;\uplus\;\texttt{ptpoly}$			$\llbracket$ ptpoly $\rrbracket$ $+$ $\llbracket$ ptpoly $\rrbracket$
		$S_{I}\;.\;\mathbf{P}_{\emptyset}$			$1$

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 2 . 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.

N°	Conditions on $S,U,V,T$	$S.\mathbf{P}_{U}\,\odot\,T.\mathbf{P}_{V}$	$\mathrm{Size}$
1	$(S=U=\emptyset)\,\lor\,(T=V=\emptyset)$	$S_{\emptyset}.\mathbf{P}_{\emptyset}$	1
2	$S=S_{I}\,\land\,U=\emptyset$	$T.\mathbf{P}_{V}$	1
3	$T=S_{I}\,\land\,V=\emptyset$	$S.\mathbf{P}_{U}$	1
4	$U=V=\emptyset$	$(S\cup T).\mathbf{P}_{\emptyset}$	1
5	$U=\emptyset\,\land\,S\cap V=\emptyset$	$(S\cup T).\mathbf{P}_{V}$	1
6	$V=\emptyset\,\land\,T\cap U=\emptyset$	$(S\cup T).\mathbf{P}_{U}$	1

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.

Explore similar work

Aug 19, 2026

Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.

Dmitry V. Alexandrov

HSE University, Moscow, Russia.

Constraint Satisfaction Formal Verification

Ask PDF

May 6, 2026

Unsat Core Prediction through Polarity-Aware Representation Learning over Clause-Literal Hypergraphs

Graph neural networks have been widely used in Boolean satisfiability (SAT) tasks to learn structural information from SAT formulas. The goal of these studies is to solve SAT instances or to enhance SAT solvers, including tasks such as unsat-core prediction. However, most existing approaches model a SAT formula as a bipartite graph or a directed acyclic graph, which are less direct in capturing clause-level and higher-order interactions among literals and clauses. Moreover, these approaches are limited in modeling intrinsic polarity-related properties of SAT, such as the complementary relationship between the positive and negative literals of a variable. To address these limitations, we propose a polarity-aware representation learning framework over clause-literal hypergraphs. We model SAT formulas as clause-literal hypergraphs augmented with a clause incidence graph to capture higher-order structural interactions. We then introduce a polarity-aware decomposition mechanism that separates variable representations into polarity invariant and equivariant components, explicitly modeling the relationship between positive and negative literals, with the resulting literal representations propagated along the hypergraph structure. We further incorporate a polarity-inversion consistency regularization to reinforce polarity-consistent representations during training. Experimental results on multiple SAT datasets demonstrate the effectiveness of the proposed approach.

Zhenchao Sun, Shuai Ma, Ping Lu +1

SKLCCSE Lab, Beihang University, Beijing, China.

Hypergraph Neural Networks Constraint Satisfaction Invariant Representation Learning

Ask PDF

Jun 15, 2026

Polynomial-Time Mistake-Bounded Language Generation

In this note, we introduce a polynomial-time version of the mistake-bounded language generation (MBLG) framework due to Kleinberg, Peale, and Reingold (2026). We observe that the family of parities of variables, and the family of conjunctions of literals, are polynomial-time MBLG. Our main result states that the family of monotone Boolean functions with polynomially-many maxterms is polynomial-time MBLG. This family includes all monotone Boolean functions, computable by polynomial-size decision trees. Our technique can be presented as a new combinatorial game about writing numbers on a board.

Héctor Jimenez, Alexander Kozachinskiy, Vicente Opazo

University of Chile · CENIA

Boolean Function Learning

Ask PDF