arXiv:2603.13854cs.LOcs.AI2026-03

提出新型多项式代数,直接高效表示布尔公式。

Power Term Polynomial Algebra for Boolean Logic

  • 用幂项多项式统一表达CNF与ANF,避免变量膨胀。
  • 支持紧凑的规范表示和局部化重写规则。
  • 适合需要结构感知的逻辑推理与转换场景。

我们引入幂项多项式代数,一种用于布尔公式的表示语言,旨在弥合合取范式(CNF)与代数正规形式(ANF)之间的表示鸿沟。传统CNF与ANF间的直接转换常导致指数级爆炸,除非通过辅助变量和附加约束将公式分解为更小片段。相比之下,我们的框架在表示层面解决这一问题,以紧凑方式编码具有结构的单项式族,并直接表示CNF子句,从而在抽象层级上避免引入辅助变量与约束。我们通过幂项与幂项多项式形式化该语言,定义其语义,并证明其支持对应于布尔多项式加法与乘法的代数运算。我们证明了该语言的关键性质:析取子句可有紧凑的规范表示;幂项支持局部缩短与展开重写规则;原子项乘积可在语言内部系统重写。这些结果共同构成一个符号演算体系,使公式可直接操作而无需展开为普通ANF。该框架提供了一种新的中间表示与重写演算,连接基于子句与代数的推理,为结构感知的CNF<->ANF转换及混合推理方法指明新方向。

原文摘要 · Abstract (English)

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.

布尔逻辑代数表示符号计算

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。