Evaluating the usefulness of Global Cardinality constraint propagators in Lazy Clause Generation

Abstract

In Constraint Programming, combinatorial problems such as those arising in the fields of artificial intelligence, scheduling, or circuit verification are modeled using mathematical constraints. Algorithms for each type of constraint are implemented in a solver and are known as propagators. Some constraints can be implemented using combinations of smaller existing propagators (this is known as decomposition), which is often used in Lazy Clause Generation (LCG) solvers, where research has shown that decompositions can be competitive or sometimes superior to purpose-built propagators for certain kinds of constraints. However, there is little research about whether a purpose-built propagator is superior to decomposition for the global cardinality constraint when used with an LCG solver. This paper benchmarks both approaches using an experimental Rust-based solver and uses existing algorithms to implement two global cardinality propagators which are then adapted for use in an LCG solver. The benchmarks show that both implementations are competitive or outperform decomposition in a dataset of 90 instances of Sudoku puzzles, being 3.19 and 2.28 times faster for Regin GAC and Basic Filter respectively. On the Minizinc Challenge dataset, the speedup factor is and 1.34 and 1.0.