Pith. sign in

REVIEW 6 minor 300 references

CSB: A Counting and Sampling tool for Bit-vectors

T0 review · 0 major / 6 minor · reviewed 2026-07-11 · grok-4.5

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

Pith's one-line read Bit-blasting plus modern CNF counters and samplers makes exact counting and uniform sampling over bit-vectors practical for the first time.

desk verdict 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. read the letter →

arxiv 2607.04142 v1 pith:VVPMKLJT submitted 2026-07-05 cs.LO cs.AI

Arijit Shaw , Kuldeep S. Meel This is my paper · ORCID
classification cs.LOcs.AI
keywords bit-vectormodelcountinguniformsamplingSMTbit-blastingprojectedCNF
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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

0 major / 6 minor

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 o AIG o CNF pipeline is argued compositionally (textbook circuits, 3-bit tests, bi-implication auxiliaries) and cross-checked against SMTApproxMC.

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 imes 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.

minor comments (6)
  1. Abstract contains a sentence fragment: “In the case of exact counting, projected counting, and uniform sampling.” Complete or remove it.
  2. Section 3.6: “Emperical assurance” is misspelled; correct to “Empirical”.
  3. 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.
  4. Table 1 reports PAR-2 averages; a short footnote clarifying that unsolved instances are charged 2 imes timeout would help readers who skip the experimental-setup paragraph.
  5. 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.
  6. 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: empirical systems paper whose claims rest on a working tool and external benchmarks, not on self-referential definitions or fitted predictions.

full rationale

The paper's central claims are engineering and empirical: (1) csb is the first tool supporting exact/projected counting and (almost-)uniform sampling over QF_BV, and (2) on 661 application benchmarks it substantially outperforms SMTApproxMC (640 vs 111 approximate counts) while also producing samples. These claims are established by construction of a pipeline (STP bit-blasting with simplifications disabled + off-the-shelf CNF counters/samplers ApproxMC/Ganak/UniGen/CMSGen + Arjun) and by direct measurement against an external baseline and a public benchmark suite. The model-preservation argument in Section 3.6 is independent of the counting numbers: it rests on textbook operator circuits (Kroening–Strichman style), compositionality over primary inputs, bi-implication auxiliaries from TechMap, 3-bit unit tests, and a cross-check that csb-exact and SMTApproxMC counts stay within the latter's (ε,δ) envelope. Self-citations to the authors' own CNF tools are used as black-box components whose correctness is established in prior literature and Model Counting Competitions; they are not invoked as uniqueness theorems that force the present result. There is no fitted parameter that is later called a prediction, no self-definitional loop, and no renaming of a known empirical pattern. Score 0 is therefore the correct outcome.

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

The work is an engineering systems paper. It inherits standard SMT and model-counting foundations and adds only the claim that a carefully disabled STP bit-blasting pipeline preserves models. No free parameters are fitted to produce the main claims; default ApproxMC tolerances are community standards. No new physical or mathematical entities are postulated.

free parameters (1)
  • ApproxMC default tolerances (ε=0.8, δ=0.2) = ε=0.8, δ=0.2
    Standard community defaults used for approximate counting mode; not fitted to the paper's own data, but they define the quality of the approximate counts reported.
assumptions (3)
  • domain assumption Modern CNF model counters (Ganak, ApproxMC) and samplers (UniGen, CMSGen) correctly count or sample the Boolean formulas they receive.
    Treated as trusted black boxes; correctness is delegated to prior literature and Model Counting Competitions (Section 3.6).
  • ad hoc to paper With all STP simplifications and substitutions disabled, the BV o AIG o CNF pipeline is model-preserving (bijection between Sol(F) and Sol(F_bit) projected onto original bits).
    Core correctness claim of the tool; justified by manual inspection of textbook circuits, 3-bit unit tests, and compositionality rather than a formal proof (Section 3.6).
  • standard math Technology-mapping CNF generation introduces only Tseitin-style auxiliary variables constrained by bi-implications, so projection onto primary inputs recovers the AIG models.
    Standard property of Tseitin/TechMap encodings (EMS07), invoked in Section 3.6.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CSB: A Counting and Sampling tool for Bit-vectors." pith.science (2026). https://pith.science/paper/VVPMKLJT

@misc{pith2026260704142,
  author       = {Pith},
  title        = {Pith review of: CSB: A Counting and Sampling tool for Bit-vectors},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VVPMKLJT}},
  note         = {Machine review of arXiv:2607.04142}
}
read the original abstract

Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, csb, that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling. Our tool csb converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. Our experiments demonstrate significant performance improvements over existing methods.

Figures

Figures reproduced from arXiv: 2607.04142 by the authors.

Figure 1
Figure 1. The architecture for counting and sampling in [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Example SMT formula with projection variables [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Performance of csb with SMTApproxMC on non-projected counting. Problem 2: Projected Model Counting As there is no existing uniform bit-vector sampling tool, we do not have a baseline for comparing csb against. We count the number of instances solved by the approximate and exact mode of csb out of 661 instances. As [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Performance comparison of two modes of csb on projected counting. Problem 3: Uniform Sampling As there is no existing uniform bit-vector sampling tool, we do not have a baseline for comparing csb against. We tested csb on our benchmarks in both sampling modes by asking…
Figure 5
Figure 5. Figure 5: Performance comparison of model counters on non-projected instances. [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]
Figure 6
Figure 6. Figure 6: Performance comparison of model counters on projected instances. [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

300 extracted references · 1 canonical work pages

  1. [1]

    2024 , publisher =

    Fichte, Johannes and Hecher, Markus and Shaw, Arijit , title =. 2024 , publisher =

    2024

  2. [2]

    International Conference on Computer Aided Verification , pages=

    Engineering an Efficient Probabilistic Exact Model Counter , author=. International Conference on Computer Aided Verification , pages=. 2025 , organization=

    2025

  3. [3]

    2025 , url =

    Model Counting Competition 2025: Description , author =. 2025 , url =

    2025

  4. [4]

    Proceedings of the 61st ACM/IEEE Design Automation Conference , pages =

    Engineering an Efficient Preprocessor for Model Counting , author =. Proceedings of the 61st ACM/IEEE Design Automation Conference , pages =

  5. [5]

    Knowledge Compilation for

    Akshay, S and Arora, Jatin and Chakraborty, Supratik and Krishna, S and Raghunathan, Divya and Shah, Shetal , booktitle =. Knowledge Compilation for

  6. [6]

    Automata-based model counting for string constraints , author =. Proc. of CAV , year =

  7. [7]

    Artificial Intelligence , year =

    SAT-based MaxSAT algorithms , author =. Artificial Intelligence , year =

  8. [8]

    What’s hard about

    Akshay , S and Chakraborty, Supratik and Goel, Shubham and Kulal, Sumith and Shah, Shetal , booktitle =. What’s hard about

Show all 300 references
  1. [9]

    Towards parallel Boolean functional synthesis , author =. Proc. of TACAS , year =

  2. [10]

    exists SAT: Projected Model Counting , author =. Proc. of SAT , year =

  3. [11]

    ACM SIGPLAN Notices , number =

    Maximal specification synthesis , author =. ACM SIGPLAN Notices , number =

  4. [12]

    Fast Sampling of Perfectly Uniform Satisfying Assignments , author =. Proc. of SAT , year =

  5. [13]

    Proceedings of the twenty-third annual ACM symposium on Theory of computing , year =

    Sampling and integration of near log-concave functions , author =. Proceedings of the twenty-third annual ACM symposium on Theory of computing , year =

  6. [14]

    Journal of Automated Reasoning , number =

    MetiTarski: An automatic theorem prover for real-valued special functions , author =. Journal of Automated Reasoning , number =

  7. [15]

    Probabilistic model counting with short XORs , author =. Proc. of SAT , year =

  8. [16]

    SAT Competition , year =

    Glucose: a solver that predicts learnt clauses quality , author =. SAT Competition , year =

  9. [17]

    Twenty-first International Joint Conference on Artificial Intelligence , year =

    Predicting learnt clauses quality in modern SAT solvers , author =. Twenty-first International Joint Conference on Artificial Intelligence , year =

  10. [18]

    International Conference on Principles and Practice of Constraint Programming , year =

    Refining restarts strategies for SAT and UNSAT , author =. International Conference on Principles and Practice of Constraint Programming , year =

  11. [19]

    International Journal on Artificial Intelligence Tools , number =

    On the Glucose SAT solver , author =. International Journal on Artificial Intelligence Tools , number =

  12. [20]

    International Conference on Computer Aided Verification , year =

    Automata-based model counting for string constraints , author =. International Conference on Computer Aided Verification , year =

  13. [21]

    B, Solimul Chowdhury and Martin, M , isbn =

  14. [22]

    Mathematics of Operations Research , number =

    A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed , author =. Mathematics of Operations Research , number =

  15. [23]

    Quantitative verification of neural networks and its security applications , year =

    Baluta, Teodora and Shen, Shiqi and Shinde, Shweta and Meel, Kuldeep S and Saxena, Prateek , booktitle =. Quantitative verification of neural networks and its security applications , year =

  16. [24]

    Thirty-First AAAI Conference on Artificial Intelligence , year =

    SAT competition 2016: Recent developments , author =. Thirty-First AAAI Conference on Artificial Intelligence , year =

    2016

  17. [25]

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems , year =

    cvc5: a versatile and industrial-strength SMT solver , author =. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , year =

  18. [26]

    Satisfiability modulo theories , year =

    Barrett, Clark and Sebastiani, Roberto and Seshia, Sanjit A and Tinelli, Cesare , booktitle =. Satisfiability modulo theories , year =

  19. [27]

    The multiple facets of software diversity: Recent developments in year 2000 and beyond , year =

    Baudry, Benoit and Monperrus, Martin , journal =. The multiple facets of software diversity: Recent developments in year 2000 and beyond , year =

    2000

  20. [28]

    AAAI/IAAI , year =

    Counting models using connected components , author =. AAAI/IAAI , year =

  21. [29]

    Brummayer, Robert and Biere, Armin , booktitle =

  22. [30]

    Stratified abstraction of access control policies , author =. Proc. of CAV , year =

  23. [31]

    Hashing-based approximate probabilistic inference in hybrid domains , author =. Proc. of UAI , year =

  24. [32]

    bioRxiv , year =

    SharpTNI: Counting and sampling parsimonious transmission networks under a weak bottleneck , author =. bioRxiv , year =

  25. [33]

    Automating the development of chosen ciphertext attacks , year =

    Beck, Gabrielle and Zinkus, Maximilian and Green, Matthew , booktitle =. Automating the development of chosen ciphertext attacks , year =

  26. [34]

    Advances in Applied Mathematics , number =

    Maximum entropy Gaussian approximations for the number of integer points and volumes of polytopes , author =. Advances in Applied Mathematics , number =

  27. [35]

    International conference on tools and algorithms for the construction and analysis of systems , year =

    Symbolic model checking without BDDs , author =. International conference on tools and algorithms for the construction and analysis of systems , year =

  28. [36]

    Lingeling, Plingeling and Treengeling entering the SAT competition 2013 , author =

    2013

  29. [37]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    Evaluating CDCL variable scoring schemes , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  30. [38]

    Pragmatics of SAT , year =

    Biere, Armin and Fr. Pragmatics of SAT , year =

  31. [39]

    Bitwuzla , author =. Proc. of CAV , year =

  32. [40]

    Resolution proofs and Skolem functions in

    Balabanov, Valeriy and Jiang, Jie-Hong R , booktitle =. Resolution proofs and Skolem functions in

  33. [41]

    Brayton, Robert and Mishchenko, Alan , booktitle =

  34. [42]

    Counting models using connected components , author =. Proc. of AAAI/IAAI , year =

  35. [43]

    Easy parameterized verification of biphase mark and 8N1 protocols , author =. Proc. of TACAS , year =

  36. [44]

    Algebraic Statistics , number =

    Sampling lattice points in a polytope: a Bayesian biased algorithm with random updates , author =. Algebraic Statistics , number =

  37. [45]

    Probabilistic inference in hybrid domains by weighted model integration , author =. Proc. of IJCAI , year =

  38. [46]

    Israel Journal of Mathematics , year =

    A quick estimate for the volume of a polyhedron , author =. Israel Journal of Mathematics , year =

  39. [47]

    2026 , publisher=

    Shaw, Arijit and Meel, Kuldeep S , journal=. 2026 , publisher=. doi:10.1007/s00236-026-00535-0 , note =

    2026 doi

  40. [48]

    ABC: An academic industrial-strength verification tool , year =

    Brayton, Robert and Mishchenko, Alan , booktitle =. ABC: An academic industrial-strength verification tool , year =

  41. [49]

    Boolector: An efficient SMT solver for bit-vectors and arrays , year =

    Brummayer, Robert and Biere, Armin , booktitle =. Boolector: An efficient SMT solver for bit-vectors and arrays , year =

  42. [50]

    Quantitative verification of neural networks and its security applications , author =. Proc. of CCS , year =

  43. [51]

    Handbook of satisfiability , year =

    Satisfiability modulo theories , author =. Handbook of satisfiability , year =

  44. [52]

    Barrett, Clark and Stump, Aaron and Tinelli, Cesare and others , booktitle =

  45. [53]

    Symmetric weighted first-order model counting , year =

    Beame, Paul and Van den Broeck, Guy and Gribkoff, Eric and Suciu, Dan , booktitle =. Symmetric weighted first-order model counting , year =

  46. [54]

    Automating the development of chosen ciphertext attacks , author =. Proc. of USENIX Security , year =

  47. [55]

    Compiling Bayesian networks with local structure , author =. Proc. of IJCAI , year =

  48. [56]

    Artificial Intelligence , year =

    On probabilistic inference by weighted model counting , author =. Artificial Intelligence , year =

  49. [57]

    Chistikov, Dmitry and Dimitrova, Rayna and Majumdar, Rupak , booktitle =

  50. [58]

    Chalkis, Apostolos and Fisikopoulos, Vissarion , journal =

  51. [59]

    Proceedings of the international conference on automated planning and scheduling , year =

    A compilation of the full PDDL+ language into SMT , author =. Proceedings of the international conference on automated planning and scheduling , year =

  52. [60]

    On parallel scalable uniform SAT witness generation , author =. Proc. of TACAS , year =

  53. [61]

    Distribution-aware sampling and weighted model counting for SAT , author =. Proc. of AAAI , year =

  54. [62]

    and Meel, Kuldeep S

    Chakraborty, Supratik and Fremont, Daniel J. and Meel, Kuldeep S. and Seshia, Sanjit A. and Vardi, Moshe Y. , title =. Proc. of TACAS , year =

  55. [63]

    Functional synthesis via input-output separation , author =. Proc. of FMCAD , year =

  56. [64]

    A scalable approximate model counter , year =

    Chakraborty, Supratik and Meel, Kuldeep S and Vardi, Moshe Y , booktitle =. A scalable approximate model counter , year =

  57. [65]

    Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls

    Chakraborty, Supratik and Meel, Kuldeep S and Vardi, Moshe Y , booktitle =. Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. , year =

  58. [66]

    Approximate model counting , year =

    Chakraborty, Supratik and Meel, Kuldeep S and Vardi, Moshe Y , journal =. Approximate model counting , year =

  59. [67]

    Approximate counting in SMT and value estimation for probabilistic programs , year =

    Chistikov, Dmitry and Dimitrova, Rayna and Majumdar, Rupak , booktitle =. Approximate counting in SMT and value estimation for probabilistic programs , year =

  60. [68]

    BOSPHORUS: bridging ANF and CNF solvers , author =. Proc. of DATE , year =

  61. [69]

    International Workshop on Fast Software Encryption , year =

    Small scale variants of the AES , author =. International Workshop on Fast Software Encryption , year =

  62. [70]

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , number =

    Cir. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , number =

  63. [71]

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems , year =

    A tool for checking ANSI-C programs , author =. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , year =

  64. [72]

    On testing of uniform samplers , author =. Proc. of AAAI , year =

  65. [73]

    Approximate probabilistic inference via word-level counting , author =. Proc. of AAAI , year =

  66. [74]

    Proceedings of the AAAI Conference on Artificial Intelligence , number =

    SMT-based verification of hybrid systems , author =. Proceedings of the AAAI Conference on Artificial Intelligence , number =

  67. [75]

    A scalable approximate model counter , author =. Proc. of CP , year =

  68. [76]

    and Vardi, Moshe Y

    Chakraborty, Supratik and Meel, Kuldeep S. and Vardi, Moshe Y. , title =. Proc. of DAC , year =

  69. [77]

    Chakraborty, Supratik and Meel, Kuldeep S and Vardi, Moshe Y , booktitle =

  70. [78]

    Handbook of Satisfiability , year =

    Approximate model counting , author =. Handbook of Satisfiability , year =

  71. [79]

    Journal of Artificial Intelligence Research , year =

    Planning for hybrid systems via satisfiability modulo theories , author =. Journal of Artificial Intelligence Research , year =

  72. [80]

    Massimo Lauria , year =

  73. [81]

    Proceedings of the third annual ACM symposium on Theory of computing , year =

    The complexity of theorem-proving procedures , author =. Proceedings of the third annual ACM symposium on Theory of computing , year =

  74. [82]

    Quantitative Evaluation of Systems , year =

    Teuber, Samuel and Weigl, Alexander , title =. Quantitative Evaluation of Systems , year =

  75. [83]

    2016 , journal =

    A Practical Volume Algorithm , author =. 2016 , journal =

    2016

  76. [84]

    Gaussian Cooling and O\^

    Cousins, Ben and Vempala, Santosh , journal =. Gaussian Cooling and O\^

  77. [85]

    cvc5: A versatile and industrial-strength SMT solver , author =. Proc. of TACAS , year =

  78. [86]

    Universal classes of hash functions , author =. Proc. of STOC , year =

  79. [87]

    Universal hashing and k-wise independent random variables via integer arithmetic without primes , author =. Proc. of STACS , year =

  80. [88]

    New advances in compiling CNF to decomposable negation normal form , author =. Proc. of ECAI , year =

  81. [89]

    Communications of the ACM , number =

    A machine program for theorem-proving , author =. Communications of the ACM , number =

  82. [90]

    SMTSampler: Efficient stimulus generation from complex SMT constraints , author =. Proc. of ICCAD , year =

  83. [91]

    Guidedsampler: coverage-guided sampling of SMT solutions , author =. Proc. of FMCAD , year =

  84. [92]

    Lemmas on demand for satisfiability solvers , author =. Proc. SAT , year =

  85. [93]

    Journal of symbolic computation , number =

    Effective lattice point counting in rational convex polytopes , author =. Journal of symbolic computation , number =

  86. [94]

    Dyer, M. E. and Frieze, A. M. , title =. SIAM Journal on Computing , number =

  87. [95]

    Journal of the ACM (JACM) , number =

    A random polynomial-time algorithm for approximating the volume of convex bodies , author =. Journal of the ACM (JACM) , number =

  88. [96]

    Descriptive complexity of \#

    Durand, Arnaud and Haak, Anselm and Kontinen, Juha and Vollmer, Heribert , journal =. Descriptive complexity of \#

  89. [97]

    An optimal algorithm for Monte Carlo estimation , year =

    Dagum, P and Karp, R and Luby, M and Ross, S , booktitle =. An optimal algorithm for Monte Carlo estimation , year =

  90. [98]

    An optimal approximation algorithm for Bayesian inference , year =

    Dagum, Paul and Luby, Michael , journal =. An optimal approximation algorithm for Bayesian inference , year =

  91. [99]

    On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing , author =. Proc. of LICS , year =

  92. [100]

    Counting-based reliability estimation for power-transmission grids , author =. Proc. of AAAI , number =

  93. [101]

    An experimental evaluation of ground decision procedures , author =. Proc. of CAV , year =

  94. [102]

    and Phan, Vu H.N

    Dudek, Jeffrey M. and Phan, Vu H.N. and Vardi, Moshe Y. , isbn =. Proc. of AAAI , keywords =

  95. [103]

    and Phan, Vu H.N

    Dudek, Jeffrey M. and Phan, Vu H.N. and Vardi, Moshe Y. , eprint =. AAAI 2020 - 34th AAAI Conference on Artificial Intelligence , keywords =

    2020

  96. [104]

    Counting-based reliability estimation for power-transmission grids , year =

    Duenas-Osorio, Leonardo and Meel, Kuldeep and Paredes, Roger and Vardi, Moshe , booktitle =. Counting-based reliability estimation for power-transmission grids , year =

  97. [105]

    A fast linear-arithmetic solver for DPLL (T) , author =. Proc. of CAV , year =

  98. [106]

    arXiv preprint arXiv:2006.15512 , year =

    Parallel weighted model counting with tensor networks , author =. arXiv preprint arXiv:2006.15512 , year =

    2006 arXiv

  99. [107]

    International conference on theory and applications of satisfiability testing , year =

    An extensible SAT-solver , author =. International conference on theory and applications of satisfiability testing , year =

  100. [108]

    Applying logic synthesis for speeding up SAT , year =

    E. Applying logic synthesis for speeding up SAT , year =. Proc. of SAT , organization =

  101. [109]

    Computational Science and Its Applications -- ICCSA 2014 , year =

    ElShaarawy, Islam and Gomaa, Walid , title =. Computational Science and Its Applications -- ICCSA 2014 , year =

    2014

  102. [110]

    Taming the curse of dimensionality: Discrete integration by hashing and optimization , author =. Proc. of ICML , year =

  103. [111]

    IJCAI International Joint Conference on Artificial Intelligence , author =

  104. [112]

    E. Proc. of SAT , year =

  105. [113]

    Sampling for bayesian program learning , author =. Proc. of Advances in Neural Information Processing Systems , year =

  106. [114]

    The model counting competition 2020 , author =

    2020

  107. [115]

    Artificial Intelligence , year =

    Sat competition 2020 , author =. Artificial Intelligence , year =

    2020

  108. [116]

    Artificial Intelligence , year =

    SAT competition 2020 , author =. Artificial Intelligence , year =

    2020

  109. [117]

    26th Annual European Symposium on Algorithms (ESA 2018) , year =

    Weighted model counting on the GPU by exploiting small treewidth , author =. 26th Annual European Symposium on Algorithms (ESA 2018) , year =

    2018

  110. [118]

    Satisfiability modulo counting: A new approach for analyzing privacy properties , author =. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science ...

  111. [119]

    Journal of computer and system sciences , number =

    Probabilistic counting algorithms for data base applications , author =. Journal of computer and system sciences , number =

  112. [120]

    International Conference on Computer Aided Verification , year =

    Early verification of legal compliance via bounded satisfiability checking , author =. International Conference on Computer Aided Verification , year =

  113. [121]

    AllSAT for Combinational Circuits , author =. Proc. of SAT , year =

  114. [122]

    27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , year =

    Entailing generalization boosts enumeration , author =. 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , year =

    2024

  115. [123]

    Lifted probabilistic inference by first-order knowledge compilation , year =

    Van den Broeck, Guy and Taghipour, Nima and Meert, Wannes and Davis, Jesse and De Raedt, Luc , booktitle =. Lifted probabilistic inference by first-order knowledge compilation , year =

  116. [124]

    AAAI , year =

    In search of the best constraint satisfaction search , author =. AAAI , year =

  117. [125]

    Fried, Dror and Tabajara, Lucas M and Vardi, Moshe Y , booktitle =

  118. [126]

    Approximate Integer Solution Counts over Linear Arithmetic Constraints , author =. Proc. of AAAI , year =

  119. [127]

    International Conference on Computer Aided Verification , pages=

    CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver , author=. International Conference on Computer Aided Verification , pages=. 2021 , organization=

    2021

  120. [128]

    A decision procedure for bit-vectors and arrays , year =

    Ganesh, Vijay and Dill, David L , booktitle =. A decision procedure for bit-vectors and arrays , year =

  121. [129]

    , author =

    Decomposition Strategies to Count Integer Solutions over Linear Constraints. , author =. Proc. of IJCAI , year =

  122. [130]

    International conference on computer aided verification , year =

    A decision procedure for bit-vectors and arrays , author =. International conference on computer aided verification , year =

  123. [131]

    A New Probabilistic Algorithm for Approximate Model Counting , year =

    Ge, Cunjing and Ma, Feifei and Liu, Tian and Zhang, Jian and Ma, Xutong , booktitle =. A New Probabilistic Algorithm for Approximate Model Counting , year =

  124. [132]

    Frontiers of Computer Science (FCS) , year =

    sharpSMT: A Scalable Toolkit for Measuring Solution Spaces of SMT(LA) Formulas , author =. Frontiers of Computer Science (FCS) , year =

  125. [133]

    Probabilistic symbolic execution , author =. Proc. of International Symposium on Software Testing and Analysis , year =

  126. [134]

    Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference , year =

    Girol, Guillaume and Farinier, Benjamin and Bardin, S. Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference , year =. International Conference on Computer Aided Verification , organization =

  127. [135]

    Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference , author =. Proc. of CAV , year =

  128. [136]

    How many bits does it take to quantize your neural network? , author =. Proc. of TACAS , year =

  129. [137]

    From sampling to model counting , author =. Proc. of IJCAI , year =

  130. [138]

    Short XORs for model counting: from theory to practice , author =. Proc. of SAT , year =

  131. [139]

    SPAA , year =

    Estimating simple functions on the union of data streams , author =. SPAA , year =

  132. [140]

    International Conference on Computer Aided Verification , year =

    Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference , author =. International Conference on Computer Aided Verification , year =

  133. [141]

    A Fast and Practical Method to Estimate Volumes of Convex Polytopes , author =. Proc. of Frontiers in Algorithmics Workshop , year =

  134. [142]

    A New Probabilistic Algorithm for Approximate Model Counting , author =. Proc. of IJCAR , year =

  135. [143]

    Cunjing Ge and Feifei Ma and Tian Liu and Jian Zhang and Xutong Ma , title =. Proc. of IJCAR , year =

  136. [144]

    Approximating integer solution counting via space quantification for linear constraints , author =. Proc. of IJCAI , year =

  137. [145]

    Handbook of satisfiability , year =

    Reasoning with quantified boolean formulas , author =. Handbook of satisfiability , year =

  138. [146]

    Ge, Cunjing and Ma, Feifei and Zhang, Peng and Zhang, Jian , journal =

  139. [147]

    Cunjing Ge and Feifei Ma and Jian Zhang , title =. Proc. of PRUV@IJCAR , year =

  140. [148]

    AAAI/IAAI , year =

    Boosting combinatorial search through randomization , author =. AAAI/IAAI , year =

  141. [149]

    Manthan: A data-driven approach for Boolean function synthesis , author =. Proc. of CAV , year =

  142. [150]

    Meel , title =

    Priyanka Golia and Subhajit Roy and Kuldeep S. Meel , title =. Proc. of IJCAI , year =

  143. [151]

    Designing samplers is easy: The boon of testers , author =. Proc. of FMCAD , year =

  144. [152]

    Engineering an efficient boolean functional synthesis engine , author =. Proc. of ICCAD , year =

  145. [153]

    Model counting: A new strategy for obtaining good bounds , author =. Proc. of AAAI , year =

  146. [154]

    Handbook of satisfiability , year =

    Model counting , author =. Handbook of satisfiability , year =

  147. [155]

    International Conference on Computer Aided Verification , year =

    Randomized synthesis for diversity and cost constraints with control improvisation , author =. International Conference on Computer Aided Verification , year =

  148. [156]

    Journal of the American statistical association , number =

    Probability inequalities for sums of bounded random variables , author =. Journal of the American statistical association , number =

  149. [157]

    Journal of heuristics , year =

    Testing heuristics: We have it all wrong , author =. Journal of heuristics , year =

  150. [158]

    Journal of Artificial Intelligence Research , year =

    The language of search , author =. Journal of Artificial Intelligence Research , year =

  151. [159]

    Software model checking for people who love automata , author =. Proc. of CAV , year =

  152. [160]

    solc-verify: A modular verifier for solidity smart contracts , author =. Proc. of VSTTE , year =

  153. [161]

    Scalable verification of quantized neural networks , author =. Proc. of AAAI , year =

  154. [162]

    , author =

    The Effect of Restarts on the Efficiency of Clause Learning. , author =. IJCAI , year =

  155. [163]

    Random Structures & Algorithms , number =

    A Bernoulli mean estimate with known relative error distribution , author =. Random Structures & Algorithms , number =

  156. [164]

    Artificial Intelligence , keywords =

    Hutter, Frank and Lindauer, Marius and Balint, Adrian and Bayless, Sam and Hoos, Holger and Leyton-Brown, Kevin , eprint =. Artificial Intelligence , keywords =

  157. [165]

    Annals of Pure and Applied Logic , number =

    A model-theoretic characterization of constant-depth arithmetic circuits , author =. Annals of Pure and Applied Logic , number =

  158. [166]

    Constraints , year =

    On computing minimal independent support and its applications to sampling and counting , author =. Constraints , year =

  159. [167]

    Quantifier elimination via functional composition , author =. Proc. of CAV , year =

  160. [168]

    Electronic Design Automation , year =

    Logic synthesis in a nutshell , author =. Electronic Design Automation , year =

  161. [169]

    ACM Communications in Computer Algebra , number =

    Solving non-linear arithmetic , author =. ACM Communications in Computer Algebra , number =

  162. [170]

    Logic synthesis in a nutshell , year =

    Jiang, Jie-Hong Roland and Devadas, Srinivas , booktitle =. Logic synthesis in a nutshell , year =

  163. [171]

    Interpolating functions from large Boolean relations , booktitle =

    Jie. Interpolating functions from large Boolean relations , booktitle =

  164. [172]

    Beaver: Engineering an efficient smt solver for bit-vector arithmetic , author =. Proc. of CAV , year =

  165. [173]

    Approximation algorithms for NP-hard problems , year =

    The Markov chain Monte Carlo method: an approach to approximate counting and integration , author =. Approximation algorithms for NP-hard problems , year =

  166. [174]

    Skolem functions for factored formulas , author =. Proc. of FMCAD , year =

  167. [175]

    Theoretical computer science , year =

    Random generation of combinatorial structures from a uniform distribution , author =. Theoretical computer science , year =

  168. [176]

    A Fast and Accurate ASP Counting Based Network Reliability Estimator , author =. Proc. of LPAR , year =

  169. [177]

    PODS , year =

    An optimal algorithm for the distinct elements problem , author =. PODS , year =

  170. [178]

    Proceedings of the twenty-ninth annual ACM symposium on Theory of computing , year =

    Sampling lattice points , author =. Proceedings of the twenty-ninth annual ACM symposium on Theory of computing , year =

  171. [179]

    FOCS , year =

    Monte-Carlo algorithms for enumeration and reliability problems , author =. FOCS , year =

  172. [180]

    , author =

    Planning as Satisfiability. , author =. ECAI , year =

  173. [181]

    Koley, Ipsita and Dey, Soumyajit and Mukhopadhyay, Debdeep and Singh, Sachin and Lokesh, Lavanya and Ghotgalkar, Shantaram Vishwanath , journal =

  174. [182]

    Complexity of

    Kov. Complexity of. 2016 , journal =

    2016

  175. [183]

    Bit-vector model counting using statistical estimation , year =

    Kim, Seonmo and McCamant, Stephen , booktitle =. Bit-vector model counting using statistical estimation , year =

  176. [184]

    Structural Bit-vector Model Counting

    Kim, Seonmo and McCamant, Stephen , booktitle =. Structural Bit-vector Model Counting. , year =

  177. [185]

    Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters , author =. Proc. of CP , year =

  178. [186]

    Discrete & Computational Geometry , year =

    Isoperimetric problems for convex bodies and a localization lemma , author =. Discrete & Computational Geometry , year =

  179. [187]

    Random Structures & Algorithms , number =

    Random walks and an o*(n5) volume algorithm for convex bodies , author =. Random Structures & Algorithms , number =

  180. [188]

    Bit-vector model counting using statistical estimation , author =. Proc. of TACAS , year =

  181. [189]

    Efficient symbolic integration for probabilistic inference , author =. Proc. of IJCAI , year =

  182. [190]

    The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability , author =

  183. [191]

    Kroening, Daniel and Strichman, Ofer , title =

  184. [192]

    Decision procedures , author =

  185. [193]

    2020 , eprint =

    Can Q -Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? , author =. 2020 , eprint =

    2020

  186. [194]

    Sampling lattice points , author =. Proc. of STOC , year =

  187. [195]

    Computational results of an

    Lov. Computational results of an. European journal of operational research , number =

  188. [196]

    arXiv preprint arXiv:1807.08058 , year =

    Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning , author =. arXiv preprint arXiv:1807.08058 , year =

    arXiv

  189. [197]

    Haifa Verification Conference , year =

    Understanding VSIDS branching heuristics in conflict-driven clause-learning SAT solvers , author =. Haifa Verification Conference , year =

  190. [198]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    Learning rate based branching heuristic for SAT solvers , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  191. [199]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    An empirical study of branching heuristics through the lens of global learning rate , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  192. [200]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    Machine learning-based restart policy for CDCL SAT solvers , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  193. [201]

    The Computer Journal , year =

    Strongly universal string hashing is fast , author =. The Computer Journal , year =

  194. [202]

    2014 IEEE International Conference on Robotics and Automation (ICRA) , year =

    A sampling-based strategy planner for nondeterministic hybrid systems , author =. 2014 IEEE International Conference on Robotics and Automation (ICRA) , year =

    2014

  195. [203]

    , author =

    Improving Model Counting by Leveraging Definability. , author =. Proc. of IJCAI , year =

  196. [204]

    Artificial Intelligence , year =

    Definability for model counting , author =. Artificial Intelligence , year =

  197. [205]

    , author =

    An Improved Decision-DNNF Compiler. , author =. Proc. of IJCAI , year =

  198. [206]

    A recursive algorithm for projected model counting , author =. Proc. of AAAI , year =

  199. [207]

    Handbook of satisfiability , year =

    MaxSAT, hard and soft constraints , author =. Handbook of satisfiability , year =

  200. [208]

    The power of literal equivalence in model counting , author =. Proc. of AAAI , year =

  201. [209]

    Proceedings [1990] 31st annual symposium on foundations of computer science , year =

    The mixing rate of Markov chains, an isoperimetric inequality, and computing the volume , author =. Proceedings [1990] 31st annual symposium on foundations of computer science , year =

    1990

  202. [210]

    How to compute the volume? , author =

  203. [211]

    Random structures & algorithms , number =

    Random walks in a convex body and an improved volume algorithm , author =. Random structures & algorithms , number =

  204. [212]

    Journal of Computer and System Sciences , number =

    Simulated annealing in convex bodies and an O*(n4) volume algorithm , author =. Journal of Computer and System Sciences , number =

  205. [213]

    Proceedings., 33rd Annual Symposium on Foundations of Computer Science , year =

    On the randomized complexity of volume and diameter , author =. Proceedings., 33rd Annual Symposium on Foundations of Computer Science , year =

  206. [214]

    Proceedings of the 26th International Joint Conference on Artificial Intelligence , year =

    An effective learnt clause minimization approach for CDCL SAT solvers , author =. Proceedings of the 26th International Joint Conference on Artificial Intelligence , year =

  207. [215]

    Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation , year =

    A model counter for constraints over unbounded strings , author =. Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation , year =

  208. [216]

    Proceedings of the thirty-sixth annual ACM symposium on Theory of computing , year =

    Hit-and-run from a corner , author =. Proceedings of the thirty-sixth annual ACM symposium on Theory of computing , year =

  209. [217]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    SAT in bioinformatics: Making the case with haplotype inference , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  210. [218]

    Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , year =

    Sparse hashing for scalable approximate model counting: theory and practice , author =. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science , year =

  211. [219]

    Technical Report MSR-TR-2007-164, Microsoft Research , year =

    Upper and lower bounds on the number of solutions , author =. Technical Report MSR-TR-2007-164, Microsoft Research , year =

    2007

  212. [220]

    IEEE Transactions on Computers , number =

    GRASP: A search algorithm for propositional satisfiability , author =. IEEE Transactions on Computers , number =

  213. [221]

    Handbook of satisfiability , year =

    Conflict-driven clause learning SAT solvers , author =. Handbook of satisfiability , year =

  214. [222]

    Upper and lower bounds on the number of solutions , year =

    Martin, Jean-Philippe , journal =. Upper and lower bounds on the number of solutions , year =

  215. [223]

    Cimatti, Alessandro and Griggio, Alberto and Schaafsma, Bastiaan Joost and Sebastiani, Roberto , booktitle =

  216. [224]

    Dualizing projected model counting , author =. Proc. of ICTAI , year =

  217. [225]

    Model Counting Competition Data Format (version 1.1) , author =

  218. [226]

    Volume computation for boolean combination of linear arithmetic constraints , author =. Proc. of CADE , year =

  219. [227]

    Cosa: Integrated verification for agile hardware design , author =. Proc. of FMCAD , year =

  220. [228]

    arXiv preprint arXiv:2012.01323 , year =

    The Model Counting Competition 2020 , author =. arXiv preprint arXiv:2012.01323 , year =

    2020 arXiv

  221. [229]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    Backing backtracking , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  222. [230]

    EPiC Series in Computing , year =

    Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting , author =. EPiC Series in Computing , year =

  223. [231]

    Proceedings of the 38th annual Design Automation Conference , year =

    Chaff: Engineering an efficient SAT solver , author =. Proceedings of the 38th annual Design Automation Conference , year =

  224. [232]

    On testing of samplers , author =. Proc. of NeurIPS , year =

  225. [233]

    Efficient weighted model integration via SMT-based predicate abstraction , author =. Proc. of AAAI , year =

  226. [234]

    Artificial Intelligence , year =

    Advanced SMT techniques for weighted model integration , author =. Artificial Intelligence , year =

  227. [235]

    and Vinodchandran, N.V

    Meel, Kuldeep S. and Vinodchandran, N.V. and Chakraborty, Sourav , title =. Proceedings of the 40th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems , numpages =. 2021 , isbn =

    2021

  228. [236]

    International Conference on Theory and Applications of Satisfiability Testing , year =

    Chronological backtracking , author =. International Conference on Theory and Applications of Satisfiability Testing , year =

  229. [237]

    Proceedings of the SAT competition , year =

    Instance generator for encoding preimage, second-preimage, and collision attacks on SHA-1 , author =. Proceedings of the SAT competition , year =

  230. [238]

    ASTAR and NTU and NUS and SUTD , title =

  231. [239]

    2016 , school =

    Improving SAT solvers by exploiting empirical characteristics of CDCL , author =. 2016 , school =

    2016

  232. [240]

    Satisfiability modulo finite fields , author =. Proc. of CAV , year =

  233. [241]

    Reliability Engineering & System Safety , year =

    Principled network reliability approximation: A counting-based approach , author =. Reliability Engineering & System Safety , year =

  234. [242]

    Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , year =

    Specification synthesis with constrained Horn clauses , author =. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , year =

  235. [243]

    International conference on theory and applications of satisfiability testing , year =

    A lightweight component caching scheme for satisfiability solvers , author =. International conference on theory and applications of satisfiability testing , year =

  236. [244]

    Abstract model counting: a novel approach for quantification of information leaks , author =. Proc. of ASIACCS , year =

  237. [245]

    Enumerative Level-2 Solution Counting for Quantified Boolean Formulas (Short Paper) , author =. Proc. of CP , year =

  238. [246]

    Theory and Applications of Satisfiability Testing -- SAT 2007 , year =

    Pipatsrisawat, Knot and Darwiche, Adnan , title =. Theory and Applications of Satisfiability Testing -- SAT 2007 , year =

    2007

  239. [247]

    , author =

    CNF Encodings. , author =. Handbook of satisfiability , year =

  240. [248]

    CNF Encodings

    Prestwich, Steven David , journal =. CNF Encodings. , year =

  241. [249]

    arXiv , arxivid =:arXiv:2212.06472v1 , author =

    2022 , title =. arXiv , arxivid =:arXiv:2212.06472v1 , author =

    2022 arXiv

  242. [250]

    SMT sampling via model-guided approximation , author =. Proc. of FM , year =

  243. [251]

    QBF solver evaluation portal 2017 , year =

    2017

  244. [252]

    QBF solver evaluation portal 2018 , year =

    2018

  245. [253]

    Incremental Determinization for Quantifier Elimination and Functional Synthesis , author =. Proc. of CAV , year =

  246. [254]

    Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30 , year =

    Reluplex: An efficient SMT solver for verifying deep neural networks , author =. Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30 , year =

    2017

  247. [255]

    Artificial Intelligence , year =

    Planning as satisfiability: parallel plans and algorithms for plan search , author =. Artificial Intelligence , year =

  248. [256]

    Rabe and Sanjit A

    Markus N. Rabe and Sanjit A. Seshia , title =. Proc. of

  249. [257]

    Understanding and extending incremental determinization for

    Rabe, Markus N and Tentrup, Leander and Rasmussen, Cameron and Seshia, Sanjit A , booktitle =. Understanding and extending incremental determinization for

  250. [258]

    2004 , institution =

    Solving linear arithmetic constraints , author =. 2004 , institution =

    2004

  251. [259]

    International Workshop on Satisfiability Modulo Theories (SMT) , year =

    An SMT-LIB theory of binary floating-point arithmetic , author =. International Workshop on Satisfiability Modulo Theories (SMT) , year =

  252. [260]

    Proceedings of SAT competition , year =

    Maple lcm dist chronobt: Featuring chronological backtracking , author =. Proceedings of SAT competition , year =

  253. [261]

    The complexity of approximate counting , author =. Proc. of STOC , year =

  254. [262]

    Operations Research , number =

    Efficient Monte Carlo procedures for generating points uniformly distributed over bounded regions , author =. Operations Research , number =

  255. [263]

    Journal of Discrete Algorithms , number =

    Samer, Marko and Szeider, Stefan , issn =. Journal of Discrete Algorithms , number =

  256. [264]

    SharpTNI: Counting and sampling parsimonious transmission networks under a weak bottleneck , year =

    Sashittal, Palash and El-Kebir, Mohammed , journal =. SharpTNI: Counting and sampling parsimonious transmission networks under a weak bottleneck , year =

  257. [265]

    Ai Magazine , number =

    The international SAT solver competitions , author =. Ai Magazine , number =

  258. [266]

    Proceedings of SAT Race 2019: Solver and Benchmark Descriptions , author =

    2019

  259. [267]

    , author =

    Combining Component Caching and Clause Learning for Effective Model Counting. , author =. SAT , year =

  260. [268]

    Scoring Functions Based on Second Level Score for k-SAT with Long Clauses , journal =

    Cai, Sangsang and Luo, Chuan and Su, Kaile , year =. Scoring Functions Based on Second Level Score for k-SAT with Long Clauses , journal =

  261. [269]

    Soos, Mate and Gocht, Stephan and Meel, Kuldeep S , booktitle =

  262. [270]

    Vegard Nossum , year =

  263. [271]

    GANAK: A Scalable Probabilistic Exact Model Counter

    Sharma, Shubham and Roy, Subhajit and Soos, Mate and Meel, Kuldeep S , booktitle =. GANAK: A Scalable Probabilistic Exact Model Counter. , year =

  264. [272]

    International Conference on Computer Aided Verification , year =

    Tuning SAT checkers for bounded model checking , author =. International Conference on Computer Aided Verification , year =

  265. [273]

    Proceedings Eighth IEEE International Conference on Tools with Artificial Intelligence , year =

    Conflict analysis in search algorithms for satisfiability , author =. Proceedings Eighth IEEE International Conference on Tools with Artificial Intelligence , year =

  266. [274]

    The Best of ICCAD , year =

    GRASP—a new search algorithm for satisfiability , author =. The Best of ICCAD , year =

  267. [275]

    Soos, Mate and Meel, Kuldeep S , booktitle =

  268. [276]

    , title =

    Soos, Mate and Meel, Kuldeep S. , title =. 2022 , booktitle =

    2022

  269. [277]

    Model Counting in the Wild , author =. Proc. of KR , year =

  270. [278]

    Shaw, Arijit and Meel, Kuldeep S , booktitle =

  271. [279]

    Model counting in the wild , author =. Proc. of Knowledge Representation and Reasoning (KR) , year =

  272. [280]

    Uncertainty in Artificial Intelligence , year =

    SMT-based weighted model integration with structure awareness , author =. Uncertainty in Artificial Intelligence , year =

  273. [281]

    Artificial Intelligence , year =

    Enhancing SMT-based Weighted Model Integration by structure awareness , author =. Artificial Intelligence , year =

  274. [282]

    Clark Barrett and Pascal Fontaine and Cesare Tinelli , title =

  275. [283]

    The smt-lib standard: Version 2.0 , author =. Proc. of SMT Workshop , year =

  276. [284]

    Extending SAT Solvers to Cryptographic Problems , author =. Proc. of SAT , organization =

  277. [285]

    Tools , year =

    Grain of salt—an automated way to test stream ciphers through SAT solvers , author =. Tools , year =

  278. [286]

    BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting , year =

    Soos, Mate and Meel, Kuldeep S , booktitle =. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting , year =

  279. [287]

    Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT) , year =

    CrystalBall: Gazing in the Black Box of SAT Solving , author =. Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT) , year =

  280. [288]

    Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling , year =

    Soos, Mate and Gocht, Stephan and Meel, Kuldeep S , booktitle =. Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling , year =

  281. [289]

    arXiv preprint arXiv:2407.19946 , year =

    Engineering an efficient approximate DNF-counter , author =. arXiv preprint arXiv:2407.19946 , year =

    arXiv

  282. [290]

    , author =

    GANAK: A Scalable Probabilistic Exact Model Counter. , author =. Proc. of IJCAI , year =

  283. [291]

    Communications of the ACM , number =

    Stochastic program optimization , author =. Communications of the ACM , number =

  284. [292]

    2017 , institution =

    Improvement of projected model-counting solver with component decomposition using SAT solving in components , author =. 2017 , institution =

    2017

  285. [293]

    sharpSAT--counting models with advanced component caching and implicit BCP , year =

    Thurley, Marc , booktitle =. sharpSAT--counting models with advanced component caching and implicit BCP , year =

  286. [294]

    arXiv preprint arXiv:1504.06804 , year =

    High speed hashing for integers and strings , author =. arXiv preprint arXiv:1504.06804 , year =

    arXiv

  287. [295]

    Thurley, Marc , booktitle =

  288. [296]

    Automation of reasoning , year =

    On the complexity of derivation in propositional calculus , author =. Automation of reasoning , year =

  289. [297]

    On the complexity of derivation in propositional calculus , year =

    Tseitin, Grigori S , booktitle =. On the complexity of derivation in propositional calculus , year =

  290. [298]

    Factored Boolean functional synthesis , author =. Proc. of FMCAD , year =

  291. [299]

    Teuber, Samuel and Weigl, Alexander , title =. Proc. of Quantitative Evaluation of Systems , year =

  292. [300]

    and Grosse, Roger and Lee, Edward and Seshia, Sanjit A

    Vaezipoor, Pashootan and Lederman, Gil and Wu, Yuhuai and Maddison, Chris J. and Grosse, Roger and Lee, Edward and Seshia, Sanjit A. and Bacchus, Fahiem , eprint =

Pith tools

Reviewed July 11, 2026 · model on record in the stance chip above.