提出新方法pact，实现混合公式的近似解计数，性能远超旧方法。
Approximate SMT Counting Beyond Discrete Domains
- 基于哈希的近似计数，仅需对投影变量做对数级SMT调用
- 在3119个实例中成功完成456个，远超基线的83个
- 适用于需要高效估算混合公式解数的研究者
SMT求解器在离散与连续域上已实现复杂公式的自动化推理。近年来命题模型计数的进步，推动将SMT能力扩展至模型计数，尤其针对混合型公式。现有方法如位爆破（bit-blasting）仅限于离散变量，难以处理混合公式的离散域解投影计数。本文提出pact，一种面向混合公式的SMT模型计数器，采用基于哈希的近似计数方法，在理论上保证估计精度。pact相对于投影变量数量呈对数级的SMT求解调用次数，并利用优化的哈希函数提升效率。在大规模基准测试中表现显著优于基线方法：在3119个实例中，pact成功完成456个，而基线仅完成83个。
原文摘要 · Abstract (English)
Satisfiability Modulo Theory (SMT) solvers have advanced automated reasoning, solving complex formulas across discrete and continuous domains. Recent progress in propositional model counting motivates extending SMT capabilities toward model counting, especially for hybrid SMT formulas. Existing approaches, like bit-blasting, are limited to discrete variables, highlighting the challenge of counting solutions projected onto the discrete domain in hybrid formulas. We introduce pact, an SMT model counter for hybrid formulas that uses hashing-based approximate model counting to estimate solutions with theoretical guarantees. pact makes a logarithmic number of SMT solver calls relative to the projection variables, leveraging optimized hash functions. pact achieves significant performance improvements over baselines on a large suite of benchmarks. In particular, out of 3119 instances, pact successfully finished on 456 instances, while Baseline could finish on 83 instances.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。