提出高效精确的整数线性约束模型计数方法，显著优于现有技术。
An Exhaustive DPLL Approach to Model Counting over Integer Linear Constraints with Simplification Techniques
- 基于穷尽DPLL架构，融合混合整数规划简化技术。
- 随机基准上解决1718个实例，远超次优方法的1470个。
- 唯一能解全部4131个应用实例，适合高精度建模需求者。
线性约束是计算机科学、运筹学和优化中的基本约束之一，许多应用可归结为整数线性约束下的模型计数（MCILC）问题。本文设计了一种基于穷尽DPLL架构的精确MCILC方法，并将混合整数规划中的多种有效简化技术融入该框架以提升效率。我们在2840个随机基准和4131个应用基准上与最先进的MCILC计数器及命题模型计数器进行了对比。实验结果表明，在随机基准上，本文方法成功求解1718个实例，而当前最优方法仅解决1470个；此外，本方法是唯一能完全求解全部4131个应用实例的方法。
原文摘要 · Abstract (English)
Linear constraints are one of the most fundamental constraints in fields such as computer science, operations research and optimization. Many applications reduce to the task of model counting over integer linear constraints (MCILC). In this paper, we design an exact approach to MCILC based on an exhaustive DPLL architecture. To improve the efficiency, we integrate several effective simplification techniques from mixed integer programming into the architecture. We compare our approach to state-of-the-art MCILC counters and propositional model counters on 2840 random and 4131 application benchmarks. Experimental results show that our approach significantly outperforms all exact methods in random benchmarks solving 1718 instances while the state-of-the-art approach only computes 1470 instances. In addition, our approach is the only approach to solve all 4131 application instances.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。