TLDR: The paper introduces EDPLLSim, a new exact model counter for integer linear constraints (MCILC). Based on an exhaustive DPLL architecture and enhanced with mixed integer programming simplification techniques, EDPLLSim significantly outperforms state-of-the-art methods on both random and application benchmarks, solving more instances faster and uniquely.
The paper introduces a new method for solving a complex problem in computer science and mathematics called Model Counting over Integer Linear Constraints (MCILC). This problem involves finding out how many possible integer solutions exist for a given set of linear equations or inequalities. It’s a fundamental challenge with applications in various fields like computer science, operations research, and optimization.
MCILC is known to be a very difficult computational task. Existing approaches generally fall into two categories: approximate methods, which estimate the number of solutions, and exact methods, which aim to find the precise count. While approximate methods are useful, many applications require an exact count.
Previous exact methods have limitations. For instance, Barvinok’s algorithm, a seminal approach, doesn’t scale well to problems with many variables (typically more than 15). Other methods translate the integer linear constraints into propositional formulas and then use propositional model counters. However, these general-purpose counters are not specifically optimized for integer linear constraints and can suffer from substantial space overhead or lack specialized simplification techniques.
The authors, Mingwei Zhang, Zhenhao Gu, Liangda Fang, Cunjing Ge, Ziliang Chen, Zhao-Rong Lai, and Quanlong Guan, from institutions like Jinan University, Nanjing University, and Pengcheng Laboratory, have developed an exact approach called EDPLLSim. This method is based on an exhaustive DPLL (Davis-Putnam-Logemann-Loveland) architecture, which is a common framework for solving satisfiability problems. To make EDPLLSim more efficient, they integrated several powerful simplification techniques borrowed from mixed integer programming. These techniques help to simplify the problem by removing redundant variables and constraints, and by tightening the bounds and coefficients of the variables.
How EDPLLSim Works
The core algorithm of EDPLLSim works by recursively breaking down the problem. It first tries to simplify the system of constraints. If the system becomes trivial (either no constraints or inconsistent), it returns the count directly. Otherwise, it attempts to decompose the problem into smaller, independent sub-problems, which can be solved much faster. If decomposition into independent parts isn’t possible, it selects a variable and tries all possible integer values for that variable, recursively solving the resulting sub-problems. A caching mechanism is also used to avoid recomputing solutions for previously encountered constraint systems.
The simplification techniques are crucial for EDPLLSim’s performance. These include:
- Removing Variables: Eliminating variables whose lower and upper bounds are the same.
- Strengthening Bounds: Tightening the possible range of values for each variable based on the constraints.
- Strengthening Coefficients: Adjusting the coefficients in the constraints to make them ‘tighter’ without changing the set of solutions.
- Removing Rows: Identifying and eliminating redundant or unsatisfiable constraints. This includes methods for individual rows, parallel rows, and subset rows.
Also Read:
- New Algorithm G-CSEA Enhances Infeasibility Diagnosis in Workforce Scheduling Models
- Unlocking Optimal Solutions for Fuzzy Optimization Problems
Experimental Results
The researchers conducted extensive experiments to evaluate EDPLLSim against seven state-of-the-art exact model counters, including those for finite-domain constraint networks, integer linear constraints, and propositional logic. They used two types of benchmarks: 2840 random instances and 4131 application instances derived from real-world software analysis and temporal planning problems.
The experimental results were impressive. On random benchmarks, EDPLLSim solved 1718 instances, significantly outperforming the next best approach, SharpSAT-TD with Arjun, which solved 1470 instances. EDPLLSim was also the fastest on 1491 instances and uniquely solved 170 instances. For application benchmarks, EDPLLSim was the only approach to solve all 4131 instances, achieving an average runtime of just 0.08 seconds, which is 20 times faster than the second-fastest counter, IntCount.
This research demonstrates that tailoring the exhaustive DPLL architecture with specific simplification techniques for integer linear constraints leads to a highly effective and efficient model counter. The paper can be accessed for more technical details at arXiv:2509.13880.
