Project CMMT (Circuit Minimization Modulo Theories)

# Objective Design, mathematically formalize, and implement a state-of-the-art Boolean circuit minimizer that addresses the Minimum Circuit Size Problem (MCSP) parameterized by background theories. # Framework * Abstract Complexity over Physicality: Standard physically-aware EDA heuristics (e.g., parasitic capacitance, physical wire delay) are to be disregarded. The optimization criteria must focus purely on pushing the boundaries of structural complexity, isolating the asymptotic gate complexity and logic depth of algebraic circuits. * Circuit Minimization Modulo Theories (CMMT): The exact synthesis engine must be powered by Satisfiability Modulo Theories (SMT) rather than relying solely on raw Boolean Satisfiability (SAT). The underlying architecture is required to abstract dense circuit sub-graphs into higher-order mathematical theories (e.g., bit-vector arithmetic, finite fields $\mathbb{Z}/m\mathbb{Z}$, and uninterpreted functions) to discover mathematical redundancies that remain invisible at the flat bit-level. * Bounded-Depth Generalization: The algorithmic framework must generalize beyond standard And-Inverter Graphs to bounded-depth circuit classes, specifically targeting $AC^0[p]$ and $TC^0$. This is to be achieved by utilizing Quantified Boolean Formulas (QBF) combined with theory-specific deduction engines. # Benchmarks for Success 1. The 16-Input Barrier: Achievement of exact synthesis for arbitrary 16-input Boolean functions in sub-exponential time, breaking the traditional $\mathcal{O}(2^n)$ exact-synthesis computational bottleneck. 2. Benchmark Annihilation: Demonstration of a mathematically proven >50% reduction in size-depth products across the entire EPFL Combinational Logic Synthesis Benchmark suite compared to the current open-source state of the art. 3. Automated Formal Verification: Emission of machine-checkable proofs (via Lean 4 or Coq) alongside every output, verifying that every localized optimization achieved by SMT-guided rewriting is strictly functionally equivalent and absolutely minimal under the specified theory. Practical Utility Target: While the methodology must remain rigorously grounded in theoretical computer science, the ultimate algorithm must be compilable into a highly scalable logic compiler. This CMMT minimizer is intended to serve as the foundational synthesis tool for emerging post-Moore's law hardware architectures—specifically reversible computing frameworks, optical circuits, and hyperdimensional arrays—where achieving the absolute theoretical minimum in gate count constitutes a strict requirement for physical viability.