{"id":"9ad710af-bd95-468f-b3be-5b68618b800c","arxiv_id":"2607.04142","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":5.5,"correctness_risk":"low","formal_verification":"none","parameter_count":1,"one_line_summary":"Bit-blasting bit-vector formulas to CNF and calling modern CNF counters/samplers yields a practical first tool for exact, projected, and uniform sampling over QF_BV.","lead":"CSB is a tool that turns bit-vector SMT formulas into CNF via bit-blasting, then reuses modern CNF counters and samplers for exact/approximate (projected) counting and almost-uniform/uniform-like sampling. It is the first practical system for several of these tasks and solves far more benchmarks than prior bit-vector counters.","discovery_kind":"new_application","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The paper's central claim is empirical and engineering: csb is the first tool offering exact/projected counting and (almost-)uniform sampling for QF_BV, and it dramatically outperforms the prior specialized approximate counter on a large application suite. The only non-trivial correctness hinge is the model-preserving property of the carefully de-simplified STP bit-blasting path. The authors supply a clear compositional argument, unit tests, and an empirical consistency check; the claim does not rest on free parameters or circular reasoning. Because the work is systems-oriented and the artifacts are public, residual risk is low and does not warrant changing the ACCEPT verdict. The concrete test above would still be a useful independent sanity check but is not expected to overturn the result.","tokens_in":13211,"tokens_out":439,"duration_ms":4576,"concrete_test":"On a random 50-instance subset of the 661 benchmarks, independently re-encode each formula with a second bit-blaster (e.g., Bitwuzla or Boolector with all rewrites off) and compare exact Ganak counts (or ApproxMC counts within the stated ε) against csb; any systematic mismatch larger than the approximation tolerance would falsify model preservation.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest assumption (model-preservation of the BV\to AIG\to CNF pipeline with STP simplifications disabled) is the natural soft spot, but it does not undermine the central claim. Section 3.6 gives a compositional argument: each operator is a standard textbook circuit (Kroening–Strichman style bi-implications), composition preserves the bijection over primary inputs, and technology-mapping CNF introduces only bi-implication auxiliaries. Empirical cross-checks against SMTApproxMC further bound the discrepancy. For a systems paper whose strongest claim is engineering (first tool + large empirical gains on 661 benchmarks), this level of assurance is standard and sufficient; a machine-checked proof would be nicer but is not required for the claim to hold.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper presents csb, a tool that extends the SMT solver STP by bit-blasting quantifier-free bit-vector formulas to CNF (with independent-support tracking and STP simplifications disabled) and then invoking off-the-shelf CNF counters (Ganak, ApproxMC) and samplers (UniGen, CMSGen) plus the Arjun preprocessor. It claims to be the first tool supporting exact and approximate projected/non-projected model counting as well as almost-uniform and uniform-like sampling over bit-vectors. On a suite of 661 application benchmarks (cryptography, software reliability, robust reachability), csb-approx counts 640 instances versus 111 for SMTApproxMC, csb-exact counts 418 (non-projected) / 643 (projected), and sampling modes produce 500 samples with median times of 1.17 s (uniform-like) and 78.4 s (almost-uniform). Correctness of the BV\to AIG\to CNF pipeline is argued compositionally (textbook circuits, 3-bit tests, bi-implication auxiliaries) and cross-checked against SMTApproxMC.","tokens_in":13389,"tokens_out":721,"duration_ms":5828,"significance":"If the empirical claims hold, the work supplies the first practical, publicly available solution for exact counting, projected counting, and uniform sampling over QF_BV, closing a long-standing gap relative to the mature CNF ecosystem. The 5–6\times improvement over SMTApproxMC on a large, application-derived suite, the open-source integration, and the extended SMT-LIB projection syntax are concrete engineering contributions that can immediately enable quantitative verification, cryptographic analysis, and reliability estimation. The modular design also means future CNF advances transfer automatically. The model-preservation argument, while not machine-checked, is standard for systems papers of this type and is buttressed by empirical cross-validation; the absence of a formal proof does not undercut the central engineering claim.","major_comments":[],"minor_comments":[{"comment":"Abstract contains a sentence fragment: “In the case of exact counting, projected counting, and uniform sampling.” Complete or remove it.","section":null},{"comment":"Section 3.6: “Emperical assurance” is misspelled; correct to “Empirical”.","section":null},{"comment":"Figure 1 caption and surrounding text: the architecture diagram is helpful, but the legend for the two parallel frameworks could be tightened so that the shared bit-blasting box is unambiguous.","section":null},{"comment":"Table 1 reports PAR-2 averages; a short footnote clarifying that unsolved instances are charged 2\times timeout would help readers who skip the experimental-setup paragraph.","section":null},{"comment":"Related-work discussion of word-level hashing (CMMV16) and statistical estimators (KM18) is accurate but could briefly note why 3-wise independence is required for sampling, making the CNF reduction more natural.","section":null},{"comment":"The extended SMT-LIB syntax with declare-projvar is useful; a one-sentence pointer to the corresponding CNF competition format (FHS24b) already present in the text could be moved earlier for readers implementing front-ends.","section":null}],"recommendation":"accept","confidential_remarks":"The manuscript is a solid systems contribution whose novelty is primarily engineering (first tool + large empirical gains). The self-citation density to the authors’ own CNF tools is expected and not problematic. Fit for Acta Informatica is appropriate; no scope or ethical concerns."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This is a clean engineering result. Shaw and Meel show that bit-blasting QF_BV into CNF and then calling current counters/samplers (Ganak, ApproxMC, UniGen, CMSGen, Arjun) inside STP gives you the first tool that actually does exact counting, projected counting, and uniform-like/almost-uniform sampling on bit-vectors. On 661 application benchmarks the numbers are unambiguous: csb-approx finishes 640 instances versus 111 for SMTApproxMC; exact mode still beats the prior approximate baseline; sampling 500 solutions is fast (median ~1 s uniform-like). Code and data are public.\n\nWhat is new is the full spectrum plus the integration, not the high-level idea. CDM15 already bit-blasted for approximate counting; the advance is that modern CNF engines are now strong enough that the reduction wins, and that they carefully keep independent support and projection sets so the CNF tools can exploit them. The architecture diagram and the three-phase sampling pipeline are clear. Disabling STP’s simplifications to preserve models is the right engineering choice and is documented.\n\nThe soft spot is exactly the one the reader flagged: model preservation of BV\to AIG\to CNF rests on textbook circuits, 3-bit unit tests, compositionality, and cross-checks against SMTApproxMC rather than a machine-checked proof. For a systems paper whose claim is “first working tool + large empirical gains,” that level of assurance is standard and sufficient; it does not undercut the performance results. Minor points: default ApproxMC tolerances are the usual community defaults, and the projected-variable syntax is a reasonable SMT-LIB extension.\n\nThis is for people who need quantitative analysis over bit-vectors (crypto, software reliability, verification). Anyone building or using SMT tools for counting/sampling will get immediate value. The math is ordinary, the data are solid, the citations are appropriate. I would send it to peer review without hesitation; it is ready for a serious referee.","headline":"Solid systems paper: first practical exact/projected/uniform tool for QF_BV via bit-blasting + modern CNF engines, with large empirical gains that hold up.","tokens_in":13973,"tokens_out":500,"would_cite":true,"duration_ms":4566,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Bit-blasting plus modern CNF counters and samplers makes exact counting and uniform sampling over bit-vectors practical for the first time.","keywords":["bit-vector","model counting","uniform sampling","SMT","bit-blasting","projected counting","CNF"],"falsifier":"An independently verified bit-vector formula for which an exact CNF count after the described blasting differs from the true number of bit-vector models would falsify the reduction.","tokens_in":14078,"feed_emoji":"⚙️","tokens_out":845,"duration_ms":7203,"temperature":0.7,"pith_summary":"Modern SMT solvers are excellent at deciding whether a bit-vector formula has any solution, yet many applications need to know how many solutions exist or to draw solutions uniformly at random. The paper shows that the answer need not wait for specialized word-level algorithms: convert the formula to CNF by bit-blasting, then hand the result to today’s mature CNF model counters and samplers. The resulting tool, csb, is the first system that performs exact model counting, projected counting, and uniform sampling over quantifier-free bit-vectors. On 661 benchmarks drawn from cryptography and software verification it approximately counts 640 instances (versus 111 for the previous best bit-vector counter) and produces hundreds of uniform-like samples in a few seconds. If the reduction is faithful, every future advance in propositional counting and sampling immediately becomes available for bit-vector problems.","feed_headline":"First practical exact counting and sampling for bit-vectors","feed_subtitle":"Bit-blast then reuse CNF counters: 640 of 661 instances solved, samples in seconds","key_machinery":"The model-preserving BV→AIG→CNF reduction: every bit-vector operator is replaced by a textbook combinational circuit whose auxiliary variables are introduced only via bi-implications, so the solutions of the original formula stand in one-to-one correspondence with the solutions of the resulting CNF projected onto the original bits.","core_discovery":"A carefully controlled bit-blasting pipeline that turns a quantifier-free bit-vector formula into an equisatisfiable CNF, followed by off-the-shelf CNF counters and samplers, yields the first practical solver for exact counting, projected counting, and (almost-)uniform sampling over bit-vectors, dramatically outperforming prior specialized word-level methods on application benchmarks.","pith_inferences":["The same reduction strategy may work for other SMT theories whose bit-blasting is known to be model-preserving, such as fixed-size arrays or floating-point.","Once exact projected counts are cheap, quantitative software-reliability tools that currently rely on sampling can switch to exact answers for small-to-medium instances.","A machine-checked formalization of the BV→CNF pipeline would remove the remaining correctness caveat and make the tool suitable for high-assurance settings."],"forward_implications":["Exact and projected model counts become available for existing cryptographic and software-reliability bit-vector benchmarks that previously had only approximate or no counts.","Uniform and almost-uniform samples can now be drawn from bit-vector solution spaces, enabling coverage-guided testing and probabilistic inference that require statistical guarantees.","Any future improvement in propositional model counters or samplers can be plugged into csb with only an API change, automatically improving bit-vector counting and sampling.","Application domains that already encode problems as bit-vector formulas can treat counting and sampling as routine library calls rather than research projects."],"fun_headline_variants":["Bit-blast bit-vectors to CNF for exact counting and sampling","CSB: Practical bit-vector counts via off-the-shelf CNF tools","Reuse CNF counters for projected bit-vector model counting","Bit-blasting pipeline enables almost-uniform bit-vector sampling","Exact bit-vector counting by converting SMT to CNF"],"cache_read_input_tokens":128,"weakest_assumption_plain":"That the bit-blasting pipeline, with all solver simplifications deliberately disabled, truly preserves a one-to-one correspondence between bit-vector solutions and CNF solutions; the paper justifies this by manual inspection of circuits and small truth-table tests rather than a machine-checked proof.","fun_headline_variants_meta":{"raw":{"variants":["Bit-blast bit-vectors to CNF for exact counting and sampling","CSB: Practical bit-vector counts via off-the-shelf CNF tools","Reuse CNF counters for projected bit-vector model counting","Bit-blasting pipeline enables almost-uniform bit-vector sampling","Exact bit-vector counting by converting SMT to CNF"]},"model":"grok-4.5","effort":"low","cost_usd":0.004296,"raw_usage":{"total_tokens":1282,"prompt_tokens":753,"num_sources_used":0,"completion_tokens":94,"cost_in_usd_ticks":42960000,"prompt_tokens_details":{"text_tokens":753,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":435,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":753,"tokens_out":94,"duration_ms":6424,"temperature":1.0,"reasoning_tokens":435,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T21:23:10.107950+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"An independently verified bit-vector formula for which an exact CNF count after the described blasting differs from the true number of bit-vector models would falsify the reduction.","supporting_citations":[],"review_version":1}