Pith. sign in

REVIEW 4 major objections 4 minor 20 references

On Top-Down Pseudo-Boolean Model Counting

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read PBMC is the first exact top-down pseudo-Boolean model counter, and it reports counting more benchmark instances in 3600 seconds than the state-of-the-art bottom-up counter PBCount.

desk verdict First exact top-down PB counter with a coefficient-aware heuristic; the performance lead is plausible but unverified without code or cross-checked counts. read the letter →

arxiv 2506.05232 v1 pith:R4FAAWGA submitted 2025-06-05 cs.LO

Suwei Yang , Yong Lai , Kuldeep S. Meel This is my paper
classification cs.LO
keywords pseudo-Booleanmodelcountingtop-downcountercoefficient-awarevariabledecisionVCISheuristicexactcomponentcachingconflict-drivensearch
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper asks whether the top-down, search-based design that made CNF model counters fast can also win for pseudo-Boolean (PB) formulas, whose constraints carry coefficients and degrees. It answers yes with PBMC, the first exact top-down PB counter, and reports that on 3500 benchmark instances PBMC returns counts for 1849 within a 3600-second timeout, while the state-of-the-art bottom-up counter PBCount returns 1773, PBCounter returns 1508, and the CNF top-down counter Ganak returns 1164. The enabling ideas are a coefficient-aware variable decision heuristic, VCIS, and a component cache that stores residual gaps and saturates them to the smallest remaining coefficient. If the claims hold, top-down search becomes a leading exact-counting method for coefficient-rich PB problems, not just for CNF.

What carries the argument

The VCIS variable decision heuristic is the central object: for variable $x$ it computes $\left(\sum_{j\in\Omega_x} b^x_j / k_j\right) \big/ |\Omega_x|$, where $b^x_j$ is the coefficient of $x$ in constraint $j$ and $k_j$ is that constraint's degree, and branches on variables in descending score with phase set to align with the largest coefficient impact. The argument also rests on the component cache, whose identity is variable IDs plus constraint IDs plus residual gaps; Lemma 2 states that matching IDs and matching gaps imply equal components, and the cache entry optimization saturates a gap to the minimum coefficient among unassigned variables when $0 < \text{gap} < \min a_j$, which is sound because any of those assignments satisfies the constraint.

What would settle it

Rerun PBCount with a systematic search over its ADD variable ordering and memory settings on the same 3500-instance suite; if any configuration counts 1850 or more instances within the same budget, PBMC's ranking claim is overturned. A second, decisive check is to find any published exact top-down PB model counter that predates PBMC, which would refute the 'first' claim.

Watch

Extended reading notes

Core claim

The central claim is that a conflict-driven top-down search, adapted to PB constraints with a coefficient-aware branching heuristic, outperforms existing exact pseudo-Boolean counters on standard benchmarks. Concretely, PBMC counts 1849 of 3500 instances in the 3600-second budget, 76 more than PBCount, and it is the only counter to solve 104 of those instances. The VCIS heuristic, which scores each variable by the sum of its coefficient-to-degree ratios across the constraints it appears in, raises the total from 1772 (using GPMC-style heuristics) to 1849, with the largest gains on multidimensional knapsack instances. A caching entry optimization that lowers the stored gap to the smallest unassigned coefficient contributes a further five instances. The paper also notes that on the sensor-placement set, where coefficients are all 1 or -1, PBMC ranks second, and it regains the lead on a cost-aware variant with non-unit coefficients.

Load-bearing premise

The load-bearing premise is that the comparison is fair: all counters ran on the same 3500 instances with the same one-core, 16 GB, 3600-second budget, and PBCount, PBCounter, and Ganak were given configurations at least as good as their published defaults, since a 76-instance lead could be erased by a modest configuration disadvantage.

Editorial extensions

If this is right

  • If PBMC's lead is real, the top-down paradigm, previously dominant only for CNF, becomes the leading exact-counting design for PB formulas, and future counters should adopt coefficient-aware branching.
  • The VCIS heuristic turns coefficient diversity into a search advantage: on multidimensional knapsack it solves 115 more instances than GPMC-style decisions, so PB-specific features should be part of counter design.
  • The cache-saturation trick improves performance even on coefficient-poor instances, suggesting that gap compression is a broadly useful engineering technique for PB search.
  • The paper's own observation that decision ordering strongly affects top-down PB counters points to adaptive heuristic selection and PB preprocessing as the next large performance levers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: coefficient-aware scoring should transfer to weighted model counting and projected PB counting, where terms also carry weights that act like surrogate coefficients.
  • Inference: a hybrid that uses VCIS to pick branch variables and tree-decomposition guidance to split components could recover the auction-set losses (VCIS loses 38 instances there) while keeping knapsack gains.
  • Inference: the gap-saturation cache entry can be ported to CDCL-based #CNF counters by treating any learnt clause as a unit-coefficient PB constraint, potentially shrinking cache keys.
  • Inference: the paper's sensor-placement results predict that as PB benchmarks become more coefficient-diverse, the top-down vs bottom-up gap will widen in PBMC's favor, a testable claim for future benchmark suites.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper introduces PBMC, a prototype exact pseudo-Boolean model counter based on a top-down, search-based design with component caching, CDCL-style conflict analysis adapted from RoundingSat, and a new variable decision heuristic called VCIS that incorporates coefficient information. The authors report that PBMC counts 1849 of 3500 benchmark instances within a 3600-second timeout, compared with 1773 for PBCount, 1508 for PBCounter, and 1164 for Ganak, and they present ablation experiments showing that VCIS and a cache-entry optimization improve the number of instances counted. The paper argues that this demonstrates the viability of top-down design for exact PB model counting.

Significance. If the reported results are correct, the paper makes a useful contribution: it is the first exact top-down PB model counter and its evaluation suggests a top-down design can be competitive with, and on these benchmarks slightly superior to, bottom-up PB counters. The evaluation is structured sensibly: it uses a common benchmark suite, a 3600-second timeout, one core and 16 GB per instance, and it reports instance counts as well as cactus plots, with ablations for the two proposed optimizations. That said, the central claim is entirely empirical, and the paper provides no artifact, no per-instance data, no cross-check of returned counts, and no formal correctness statement for the counter as a whole. The absence of output validation is particularly consequential because the headline margin over PBCount is only 76 instances. The contribution is therefore plausible but not yet established at the standard expected for a tool paper.

major comments (4)
  1. [Section 4.2, Table 1] The headline claim is that PBMC returns counts for 1849 instances versus 1773 for PBCount, but the paper never validates that the returned numbers are the correct model counts. There is no ground-truth check on small instances, no agreement check against PBCount or PBCounter on instances solved by both tools, and no per-instance count list. Because PBMC is a new prototype combining propagation, learned constraints, backjumping, and a new caching scheme, an implementation bug could cause it to terminate quickly with a wrong count, artificially inflating the number of 'counted' instances. With a margin of only 76 instances, even a small number of miscounts would erase or reverse the claimed lead. The manuscript should add correctness validation, for example by checking counts on small instances with brute force, by cross-checking counts on overlapping solved instances, and by releasing the per-instance outputs.
  2. [Section 4.1] The experimental setup does not specify the versions, command-line options, or input encodings for the competing counters. In particular, Ganak is a CNF model counter, yet the paper does not explain how Ganak was applied to PB benchmark instances; if a PB-to-CNF encoding was used, the encoding choice and parameters need to be reported. Similarly, PBCount and PBCounter may have configuration options that affect performance, and the paper only states that the same benchmark suite as prior work [19] was used. Since the lead over PBCount is small (76 instances), an unfair or suboptimal configuration for a competitor could change the ranking. The authors should provide exact commands, versions, and encoding details, ideally as runnable scripts.
  3. [Section 3, Algorithms 1 and 2] The paper describes PBMC as an exact counter but does not provide a correctness theorem or invariant for the overall algorithm. Lemma 2 only justifies the cache key; it does not establish that Count and CountPBMC return the model count under propagation, conflict analysis, learned constraints, backjumping, and component decomposition. The need for such an argument is made concrete by the conflict branch in Algorithm 2: line 4 stores zeta[phi] = 0 before conflict analysis, and then line 6 backjumps and 'clears related cache and recursive calls,' but the pseudocode does not explain how the cached 0 is prevented from being reused at the backjump target. At minimum, the authors should add a detailed proof sketch or a rigorous invariant, or strengthen the empirical validation to compensate for the absence of a formal correctness argument.
  4. [Section 3.2 and Table 2] The VCIS heuristic is described only as an 'equal-weighted additional component' to prior GPMC heuristics, but the exact blending formula is not given, and no sensitivity analysis is reported. Table 2 shows that VCIS loses 38 instances on Auction while gaining 115 on M-dim Knapsack, so the overall benefit is a property of this particular benchmark mix and this particular equal-weight choice. The paper should define the combined decision score precisely, state whether the equal weight was tuned or fixed a priori, and report how sensitive the results are to the weighting.
minor comments (4)
  1. [Section 4.2] The cost-aware sensor placement experiment is mentioned only in prose ('PBMC outperforms PBCount by returning counts for 715 instances whereas PBCount could only return for 678 instances'), with no table, benchmark-generation details, or timeout description; this result should be presented with the same rigor as the other experiments.
  2. [Section 3.2] The VCIS score formula is typeset inline and not numbered; numbering it (or giving it as a display equation) would make it easier to refer to in future work.
  3. [Section 3.3] The gap-saturation optimization is described only for the case 0 < s < min a_j; the paper should clarify what happens if the minimum coefficient is not unique or if the constraint is already an equality, since the equality case is converted to a pair of inequalities earlier in Section 2.1.
  4. [References] Reference [15] lists 'Kenji Hashimoto Ryosuke Suzuki and Masahiko Sakai'; the author boundaries are unclear and the entry should be formatted consistently with the other references.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: PBMC's claims are empirical comparisons with hand-designed heuristics on external benchmarks, not derived from its own outputs.

full rationale

The paper makes no derivation that collapses into its own inputs. PBMC is a new top-down pseudo-Boolean counter whose design choices, including the VCIS variable decision heuristic and cache saturation, are justified by explicit intuitions and soundness arguments rather than by assuming the target counts. The central performance claims are empirical: PBMC's reported ability to count 1849 instances versus 1773 for PBCount is measured on a fixed external benchmark suite under a stated timeout, and the VCIS ablation compares two concrete configurations. The cited prior work by the same authors provides building blocks and baselines, but the load-bearing evidence is the runtime comparison, not the citations themselves. Even the component-caching correctness argument in Lemma 2 is a self-contained equivalence proof, and the cache-entry saturation is justified by a direct soundness observation about gaps. The paper does not rename a known result or fit a parameter to the test set. The absence of a ground-truth validation of the returned counts is a legitimate experimental concern but is not a circularity in the derivation chain.

Assumptions & free parameters 1 free parameters · 3 assumptions · 0 invented entities

The paper's contributions are algorithmic and experimental; it introduces no new theoretical entities. The central correctness argument rests on standard search-based counting (DPLL with component caching) and the normalization of PB constraints; the only hand-set design choice is the equal-weight blending in VCIS, which is noted as a free parameter.

free parameters (1)
  • VCIS equal-weight blending factor = 1 (equal weight with GPMC score)
    The VCIS score is added as an equal-weighted component to the existing GPMC variable decision heuristic (Section 3.2). The weight is chosen by hand, not fitted, and no sensitivity analysis is provided; the Auction benchmark shows VCIS can reduce solved instances (503 vs 541 for GPMC-heu), indicating the blend is not universally optimal.
assumptions (3)
  • domain assumption Standard DPLL-style search with component caching is sound for exact counting.
    PBMC's Count algorithm (Algorithm 2) assumes that branching on a variable sums the counts of the two branches and that variable-disjoint components multiply, following the top-down counting paradigm from CNF counters (Section 2.3).
  • standard math PB constraints can be normalized to the form sum a_i x_i >= k with positive coefficients without changing the model count.
    Section 2.1 states that <= constraints are converted by multiplying by -1, = constraints by a pair of inequalities, and negative coefficients by substituting x = 1 - x. These are algebraic identities.
  • domain assumption The component caching scheme identifies a component by variable IDs, constraint IDs, and current gaps, and this identification is sufficient for reuse.
    Lemma 2 provides a proof sketch that equal IDs and gaps imply equal counting subproblems, and Section 3.3 describes the cache key construction. The implementation assumes IDs are stable and gap saturation preserves the count.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On Top-Down Pseudo-Boolean Model Counting." pith.science (2026). https://pith.science/paper/R4FAAWGA

@misc{pith2026250605232,
  author       = {Pith},
  title        = {Pith review of: On Top-Down Pseudo-Boolean Model Counting},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/R4FAAWGA}},
  note         = {Machine review of arXiv:2506.05232}
}
read the original abstract

Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased interest partly owing to the succinctness of PB formulas over typical propositional Boolean formulas in conjunctive normal form (CNF) at describing problem constraints. In particular, the research community has developed tools to tackle exact PB model counting. These recently developed counters follow one of the two existing major designs for model counters, namely the bottom-up model counter design. A natural question would be whether the other major design, the top-down model counter paradigm, would be effective at PB model counting, especially when the top-down design offered superior performance in CNF model counting literature. In this work, we investigate the aforementioned top-down design for PB model counting and introduce the first exact top-down PB model counter, PBMC. PBMC is a top-down search-based counter for PB formulas, with a new variable decision heuristic that considers variable coefficients. Through our evaluations, we highlight the superior performance of PBMC at PB model counting compared to the existing state-of-the-art counters PBCount, PBCounter, and Ganak. In particular, PBMC could count for 1849 instances while the next-best competing method, PBCount, could only count for 1773 instances, demonstrating the potential of a top-down PB counter design.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

20 extracted references · 19 canonical work pages

  1. [19]

    Suwei Yang and Kuldeep S. Meel. Engineering an exact pseudo-boolean model counter. In Proceedings of the 38th Annual AAAI Conference on Artificial Intelligence , 2024

    work page 2024

  2. [1]

    Iris Bahar, Erica A

    R. Iris Bahar, Erica A. Frohm, Charles M. Gaona, Gary D. Hachtel, Enrico Macii, Abelardo Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. In International Conference on Computer Aided Design , 1993

    work page 1993

  3. [2]

    Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers , C-35(8):677--691, 1986. https://doi.org/10.1109/TC.1986.1676819 doi:10.1109/TC.1986.1676819

    arXiv 1986

  4. [3]

    Dudek, Vu Hoang Nguyen Phan, and Moshe Y

    Jeffrey M. Dudek, Vu Hoang Nguyen Phan, and Moshe Y. Vardi. Addmc: Weighted model counting with algebraic decision diagrams. In AAAI Conference on Artificial Intelligence , 2020

    work page 2020

  5. [4]

    Dudek, Vu Hoang Nguyen Phan, and Moshe Y

    Jeffrey M. Dudek, Vu Hoang Nguyen Phan, and Moshe Y. Vardi. Dpmc: Weighted model counting by dynamic programming on project-join trees. In International Conference on Principles and Practice of Constraint Programming , 2020

    work page 2020

  6. [5]

    Dudek, Vu Hoang Nguyen Phan, and Moshe Y

    Jeffrey M. Dudek, Vu Hoang Nguyen Phan, and Moshe Y. Vardi. Procount: Weighted projected model counting with graded project-join trees. In International Conference on Theory and Applications of Satisfiability Testing , 2021

    work page 2021

  7. [6]

    Meel, Roger Paredes, and Moshe Y

    Leonardo Due \ n as-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In AAAI Conference on Artificial Intelligence , 2017

    work page 2017

  8. [7]

    Divide and conquer: Towards faster pseudo-boolean solving

    Jan Elffers and Jakob Nordstr \"o m. Divide and conquer: Towards faster pseudo-boolean solving. In International Joint Conference on Artificial Intelligence (IJCAI) , 2018

    work page 2018

Show all 20 references
  1. [8]

    \#sat-based vulnerability analysis of security components — a case study

    Linus Feiten, Matthias Sauer, Tobias Schubert, Alexander Czutro, Eberhard B \"o hl, Ilia Polian, and Bernd Becker. \#sat-based vulnerability analysis of security components — a case study. 2012 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnolo...

    2012

  2. [9]

    Mohimenul Kabir, Supratik Chakraborty, and Kuldeep S. Meel. Exact asp counting with compact encodings. AAAI Conference on Artificial Intelligence , 2024

    2024

  3. [10]

    Mohimenul Kabir, Flavio Everardo, Ankit Shukla, Markus Hecher, Johannes Klaus Fichte, and Kuldeep S. Meel. Approxasp - a scalable approximate answer set counter. In AAAI Conference on Artificial Intelligence , 2022

    2022

  4. [11]

    Integrating tree decompositions into decision heuristics of propositional model counters

    Tuukka Korhonen and Matti J \"a rvisalo. Integrating tree decompositions into decision heuristics of propositional model counters. In International Conference on Principles and Practice of Constraint Programming , 2021

    2021

  5. [12]

    An improved decision-dnnf compiler

    Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In International Joint Conference on Artificial Intelligence , 2017

    2017

  6. [13]

    Pbcounter: weighted model counting on pseudo-boolean formulas

    Yong Lai, Zhenghang Xu, and Minghao Yin. Pbcounter: weighted model counting on pseudo-boolean formulas. Frontiers of Computer Science , 19:193402, 2024

    2024

  7. [14]

    Pseudo-boolean constraints from a knowledge representation perspective

    Daniel Le Berre , Pierre Marquis, Stefan Mengel, and Romain Wallon. Pseudo-boolean constraints from a knowledge representation perspective. In International Joint Conference on Artificial Intelligence , 2018

    2018

  8. [15]

    Improvement of projected model-counting solver with component decomposition using sat solving in components

    Kenji Hashimoto Ryosuke Suzuki and Masahiko Sakai. Improvement of projected model-counting solver with component decomposition using sat solving in components. In JSAI Technical Report , 3 2017

    2017

  9. [16]

    Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In AAAI Conference on Artificial Intelligence , 2005

    2005

  10. [17]

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. Ganak: A scalable probabilistic exact model counter. In Proceedings of International Joint Conference on Artificial Intelligence , 8 2019

    2019

  11. [18]

    Jiong Yang and Kuldeep S. Meel. Engineering an efficient pb-xor solver. In International Conference on Principles and Practice of Constraint Programming , 2021

    2021

  12. [20]

    Suwei Yang and Kuldeep S. Meel. Towards projected and incremental pseudo-boolean model counting. In Proceedings of the 39th Annual AAAI Conference on Artificial Intelligence , 2025

    2025

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.