pith. sign in

arxiv: 2411.10037 · v3 · pith:XPHOZLARnew · submitted 2024-11-15 · 💻 cs.LO

MCAC: A Model Counting Algorithm for Exact Computation of Error Metrics of Approximate Circuits

S Ramprasath , Sibi Siddharthan , Marrivada Gopala Krishna Sai Charan , Vinita Vasudevan This is my paper

Pith reviewed 2026-05-23 17:50 UTC · model grok-4.3

classification 💻 cs.LO
keywords approximate circuitsmodel countingerror metricsCNF formulamessage passingerror miteraverage errorworst-case error
0
0 comments X

The pith

MCAC computes all error metrics for approximate circuits from one model count on a shared error miter.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces MCAC as a model counting framework that computes multiple average and worst-case error metrics exactly for approximate circuits. It does this by synthesizing a single error miter consisting of the exact circuit, approximate circuit, and a subtractor, converting its CNF formula into a tree, and applying message passing with data structures for efficient sparse computations. This replaces the need for multiple model counter calls and specialized miters required by existing methods. A reader would care because approximate circuits rely on accurate error evaluation to balance performance gains against accuracy losses.

Core claim

MCAC uses the CNF formula of a single error miter to compute all metrics by converting the formula to a tree and using message passing, with proposed data structures for sparse computations, resulting in significant speedups over off-the-shelf model counters on benchmark instances.

What carries the argument

Conversion of the CNF formula of the error miter to a tree followed by message passing for computing error metrics.

If this is right

  • All error metrics are obtained from a single synthesis of the system.
  • Exact computation of both average and worst-case error metrics.
  • Significant speedup demonstrated on several benchmark instances.
  • The same error miter serves for all metrics instead of metric-specific ones.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This tree-and-message-passing approach might apply to computing other properties of circuits beyond error metrics.
  • Scalability depends on the tree structure being efficient for larger circuits.
  • Adoption could standardize error evaluation across approximate circuit design tools.

Load-bearing premise

Converting the CNF to a tree and performing message passing with the proposed data structures yields exact error metric values and the reported speedups.

What would settle it

A test case where MCAC's computed error metrics differ from those calculated by exhaustive simulation or another exact method on the same circuit.

Figures

Figures reproduced from arXiv: 2411.10037 by Marrivada Gopala Krishna Sai Charan, Sibi Siddharthan, S Ramprasath, Vinita Vasudevan.

Figure 1
Figure 1. Figure 1: Message passing for a tree. The messages are passed [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: (a) Partitioning the CNF formula F with error variables 𝑒 and 𝑓 into F1, F2, F3 and constructing graph G (b) Merging F1 and F2 and marginalizing X1,2 w.r.t {𝑎, 𝑐} (c) Message passing 3) Merge and Marginalize: Assume that 𝑉𝑖 and 𝑉𝑗 are connected by an edge 𝐸𝑖, 𝑗. MERGE(𝐺, 𝑉𝑖 , 𝑉𝑗) replaces the two vertices by a single vertex 𝑉𝑖 associated with the formula Fi ∧ Fj and the modified variable set Xi = Xi ∪ Xj .… view at source ↗
Figure 3
Figure 3. Figure 3: Histogram of error probabilities for the BACS bench [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
read the original abstract

Effective usage of approximate circuits for various performance trade-offs requires accurate computation of error. MCAC is a novel model counting framework for exact computation of several average and worst-case error metrics that are used to evaluate approximate circuits. Unlike other methods in the literature, our framework uses the same error miter for all metrics. It requires a single synthesis of the system consisting of the exact and approximate circuits followed by a subtractor that finds the difference of the two outputs. Existing miter-based methods require multiple calls to the model counter, one for each output of the miter. MCAC uses the CNF formula of the system to compute all metrics. Our algorithm converts the formula to a tree and uses message passing to compute all metrics. We propose data structures to efficiently store and perform sparse computations required for conversion to a tree and message passing. Results for all the error metrics for several benchmark instances show a significant speedup over using off-the-shelf model counters along with specialized miters for each metric.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces MCAC, a model counting framework for exact computation of multiple average and worst-case error metrics for approximate circuits. It uses a single shared error miter (exact circuit + approximate circuit + subtractor), converts the resulting CNF to a tree, and applies message passing with custom sparse data structures to compute all metrics simultaneously, claiming significant speedups versus off-the-shelf model counters that require metric-specific miters.

Significance. If the tree conversion and message-passing rules preserve exact model counts for all metrics without truncation or aggregation errors, the single-miter approach would eliminate repeated synthesis and counting calls, providing a practical efficiency gain for approximate-circuit evaluation.

major comments (2)
  1. [Algorithm description (post-abstract)] The central claim of exactness rests on the CNF-to-tree conversion plus message passing (described in the algorithm section) being semantically equivalent to full #SAT enumeration on the original miter formula; no derivation, invariant, or equivalence proof is supplied showing that the sparse operations compute the precise cardinalities required for average/worst-case metrics.
  2. [Abstract and § on miter construction] The abstract asserts that the same miter supports all metrics via one synthesis, yet the manuscript supplies no formal argument that the tree structure and message-passing rules simultaneously recover the distinct counting queries (e.g., total error count, maximum error, etc.) without metric-specific adjustments that would undermine the single-synthesis advantage.
minor comments (1)
  1. Benchmark instances and exact speedup numbers are referenced but not enumerated with circuit sizes, metric values, or comparison baselines in the provided text.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and the constructive comments on the need for explicit justification of exactness and the single-miter property. We address the two major comments point by point below.

read point-by-point responses

  1. Referee: [Algorithm description (post-abstract)] The central claim of exactness rests on the CNF-to-tree conversion plus message passing (described in the algorithm section) being semantically equivalent to full #SAT enumeration on the original miter formula; no derivation, invariant, or equivalence proof is supplied showing that the sparse operations compute the precise cardinalities required for average/worst-case metrics.

    Authors: The tree conversion constructs a syntax tree whose nodes correspond to the clauses and variables of the miter CNF such that each subtree represents a sub-formula whose models are independent of the rest of the formula. Message passing then computes, bottom-up, the exact cardinality of models for each partial assignment at every node by summing and multiplying the child counts; the sparse data structures store only the non-zero cardinalities, introducing no truncation. Because the tree is a faithful representation of the original conjunction, the root cardinality equals the number of models of the CNF. We will add an inductive argument establishing this equivalence in the revised algorithm section. revision: yes

  2. Referee: [Abstract and § on miter construction] The abstract asserts that the same miter supports all metrics via one synthesis, yet the manuscript supplies no formal argument that the tree structure and message-passing rules simultaneously recover the distinct counting queries (e.g., total error count, maximum error, etc.) without metric-specific adjustments that would undermine the single-synthesis advantage.

    Authors: The single miter CNF encodes the numerical error value across its output bits. Message passing on the tree computes the complete distribution of this error value (i.e., the number of models for each possible magnitude) in one pass. All required metrics are then obtained by post-processing the same distribution: average error via the weighted sum, worst-case error via the largest magnitude with positive count, and similarly for the remaining metrics. No metric-specific miters or additional counting calls are required. We will add an explicit derivation of each metric from the error distribution in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No circularity; algorithmic construction is self-contained

full rationale

The paper presents MCAC as an algorithmic method: synthesize a single shared error miter (exact + approximate circuit + subtractor), convert its CNF to a tree, then apply message passing with custom sparse data structures to compute multiple error metrics exactly. No derivation step reduces to a fitted parameter, self-definition, or self-citation chain; the central claim is that the tree conversion and message-passing rules preserve exact #SAT semantics for all metrics simultaneously. This is an independent algorithmic proposal whose correctness is externally falsifiable via model counters or benchmarks, not internally forced by construction. No load-bearing self-citations or ansatzes are invoked in the provided text.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Review based on abstract only; no free parameters or invented entities are described. The approach rests on standard model-counting assumptions in logic synthesis.

axioms (2)
  • domain assumption The CNF formula of the single miter accurately encodes the error computation for all metrics
    Invoked when stating that the CNF is used to compute all metrics
  • ad hoc to paper Tree conversion plus message passing yields exact results with efficient sparse operations
    Core algorithmic step proposed in the abstract

pith-pipeline@v0.9.0 · 5718 in / 1427 out tokens · 31404 ms · 2026-05-23T17:50:54.050445+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    BDD minimization for approximate computing,

    M. Soeken, D. Große, A. Chandrasekharan, and R. Drechsler, “BDD minimization for approximate computing,” in Asia and South Pacific Design Automation Conference (ASP-DAC) , pp. 474–479, 2016

    work page 2016

  2. [2]

    Analyzing Imprecise Adders Using BDDs – A Case Study,

    C. Yu and M. Ciesielski, “Analyzing Imprecise Adders Using BDDs – A Case Study,” in IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 152–157, 2016

    work page 2016

  3. [3]

    Formal Methods for Exact Analysis of Approximate Cir- cuits,

    Z. Vasicek, “Formal Methods for Exact Analysis of Approximate Cir- cuits,” IEEE Access, vol. PP, pp. 1–1, 12 2019

    work page 2019

  4. [4]

    ALFANS: Multilevel Approximate Logic Synthesis Framework by Approximate Node Simplification,

    Y . Wu and W. Qian, “ALFANS: Multilevel Approximate Logic Synthesis Framework by Approximate Node Simplification,” IEEE Trans. Comput.- Aided Design Integr. Circuits Syst. , vol. 39, no. 7, pp. 1470–1483, 2020

    work page 2020

  5. [5]

    Optimization of BDD-based Approximation Error Metrics Calculations,

    V . Mrazek, “Optimization of BDD-based Approximation Error Metrics Calculations,” in IEEE Computer Society Annual Symposium on VLSI (ISVLSI), pp. 86–91, 2022

    work page 2022

  6. [6]

    Approximate hardware gen- eration using symbolic computer algebra employing grobner basis,

    S. Froehlich, D. Große, and R. Drechsler, “Approximate hardware gen- eration using symbolic computer algebra employing grobner basis,” in Design, Automation & Test in Europe Conference & Exhibition (DATE) , pp. 889–892, 2018

    work page 2018

  7. [7]

    One Method - All Error- Metrics: A Three-Stage Approach for Error-Metric Evaluation in Approx- imate Computing,

    S. Froehlich, D. Große, and R. Drechsler, “One Method - All Error- Metrics: A Three-Stage Approach for Error-Metric Evaluation in Approx- imate Computing,” in Design, Automation & Test in Europe Conference & Exhibition (DATE) , pp. 284–287, 2019

    work page 2019

  8. [8]

    Approximating complex arithmetic circuits with formal error guarantees: 32-bit multipliers accomplished,

    M. ˇCeˇska, J. Matya ˇs, V . Mrazek, L. Sekanina, Z. Vasicek, and T. V ojnar, “Approximating complex arithmetic circuits with formal error guarantees: 32-bit multipliers accomplished,” in IEEE/ACM International Conference on Computer-Aided Design (ICCAD) , pp. 416–423, 2017

    work page 2017

  9. [9]

    V ACSEM: Verifying Average Errors in Approximate Circuits Using Simulation- Enhanced Model Counting,

    C. Meng, H. Wang, Y . Mai, W. Qian, and G. De Micheli, “V ACSEM: Verifying Average Errors in Approximate Circuits Using Simulation- Enhanced Model Counting,” in Design, Automation & Test in Europe Conference & Exhibition (DATE) , pp. 1–6, 2024

    work page 2024

  10. [10]

    GANAK: A Scalable Probabilistic Exact Model Counter,

    S. Sharma, S. Roy, M. Soos, and K. S. Meel, “GANAK: A Scalable Probabilistic Exact Model Counter,” in Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) , 8 2019

    work page 2019

  11. [11]

    Koller and N

    D. Koller and N. Friedman, Probabilistic graphical models: principles and techniques. MIT press, 2009

    work page 2009

  12. [12]

    Guiding SAT Solving by Formula Parti- tioning,

    Z. A. Mann and P. A. Papp, “Guiding SAT Solving by Formula Parti- tioning,” International Journal on Artificial Intelligence Tools , vol. 26, no. 04, 2017

    work page 2017

  13. [13]

    High-Quality Hypergraph Partitioning,

    S. Schlag, T. Heuer, L. Gottesb ¨uren, Y . Akhremtsev, C. Schulz, and P. Sanders, “High-Quality Hypergraph Partitioning,” ACM J. Exp. Al- gorithmics, vol. 27, Feb 2023

    work page 2023

  14. [14]

    The Parallel Hashmap C++ library,

    G. Popovitch, “The Parallel Hashmap C++ library,” Jan. 2024. https://github.com/greg7mdp/parallel-hashmap

    work page 2024

  15. [15]

    HyperLogLog in practice: algo- rithmic engineering of a state of the art cardinality estimation algorithm,

    S. Heule, M. Nunkesser, and A. Hall, “HyperLogLog in practice: algo- rithmic engineering of a state of the art cardinality estimation algorithm,” in International Conference on Extending Database Technology , EDBT ’13, (New York, NY , USA), p. 683–692, ACM, 2013

    work page 2013

  16. [16]

    Approximate Logic Synthesis: A Survey,

    I. Scarabottolo, G. Ansaloni, G. A. Constantinides, L. Pozzi, and S. Reda, “Approximate Logic Synthesis: A Survey,” Proceedings of the IEEE , vol. 108, no. 12, pp. 2195–2213, 2020

    work page 2020

  17. [17]

    A low latency generic accuracy configurable adder,

    M. Shafique, W. Ahmad, R. Hafiz, and J. Henkel, “A low latency generic accuracy configurable adder,” in Design Automation Conference (DAC) , pp. 1–6, 2015

    work page 2015

  18. [18]

    Low-Power Digital Signal Processing Using Approximate Adders,

    V . Gupta, D. Mohapatra, A. Raghunathan, and K. Roy, “Low-Power Digital Signal Processing Using Approximate Adders,” IEEE Trans. Comput.-Aided Design Integr. Circuits Syst., vol. 32, no. 1, pp. 124–137, 2013

    work page 2013

  19. [19]

    Approximate XOR/XNOR-based adders for inexact computing,

    Z. Yang, A. Jain, J. Liang, J. Han, and F. Lombardi, “Approximate XOR/XNOR-based adders for inexact computing,” in IEEE International Conference on Nanotechnology (IEEE-NANO 2013) , pp. 690–693, 2013

    work page 2013

  20. [20]

    Bio-Inspired Imprecise Computational Blocks for Efficient VLSI Implementation of Soft-Computing Applications,

    H. R. Mahdiani, A. Ahmadi, S. M. Fakhraie, and C. Lucas, “Bio-Inspired Imprecise Computational Blocks for Efficient VLSI Implementation of Soft-Computing Applications,”IEEE Trans. Circuits Syst. I, vol. 57, no. 4, pp. 850–862, 2010

    work page 2010

  21. [21]

    Perron and F

    L. Perron and F. Didier, “CP-SAT,” May 2024. https://developers.google.com/optimization/cp/cp solver/

    work page 2024

  22. [22]

    Probabilistic Error Modeling for Two-part Segmented Approximate Adders,

    D. Celia, V . Vasudevan, and N. Chandrachoodan, “Probabilistic Error Modeling for Two-part Segmented Approximate Adders,” in IEEE Inter- national Symposium on Circuits and Systems (ISCAS) , pp. 1–5, 2018

    work page 2018

  23. [23]

    Efficient Error Estimation for High- Level Design Space Exploration of Approximate Computing Systems,

    M. Vaeztourshizi and M. Pedram, “Efficient Error Estimation for High- Level Design Space Exploration of Approximate Computing Systems,” IEEE Trans. VLSI Syst. , vol. 31, no. 7, pp. 917–930, 2023

    work page 2023