An Exhaustive DPLL Approach to Model Counting over Integer Linear Constraints with Simplification Techniques
This addresses the computational bottleneck of model counting for applications in computer science and optimization, representing an incremental improvement over existing exact methods.
The paper tackles the problem of exact model counting over integer linear constraints by developing an exhaustive DPLL approach with simplification techniques, achieving state-of-the-art performance by solving 1718 out of 2840 random instances (compared to 1470 for previous methods) and all 4131 application instances.
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.