Automatic Generation of Rule-Based Constraint Solvers over Finite Domains

摘要

A general approach to implement propagation and simplification of constraints consists of applying rules over these constraints. However, a difficulty that arises frequently when writing a constraint solver is to determine the constraint propagation algorithm. In this article, we propose a method for generating propagation and simplification rules for constraints over finite domains defined ex-tensionally by, for example, a truth table or their tuples. The generation of rules is performed in two steps. First, propagation rules are generated. Propagation rules do not rewrite constraints but add new ones. Thus, the constraint store may contain superfluous constraints. Removing these constraints not only allows saving of space but also decreases the cost of constraint solving. Constraints can be removed using simplification rules. Thus, in a second step, some propagation rules are transformed into simplification rules. Furthermore, we show that our approach performs well on various examples, including Boolean constraints, multivalued logic, and Allen's qualitative approach to temporal logic. Moreover, an application taken from the field of digital circuit design shows that our approach is of practical use.