Correctness considerations in CLP(FD) systems

Abstract

Constraint logic programming (CLP) is a declarative formalism for describing conditions a solution must satisfy. Constraint logic programming over finite domains, denoted as CLP(FD), considers problems involving integers, including combinatorial problems such as planning, scheduling and allocation tasks. Given a problem description, a constraint solver tries to find valid solutions via constraint propagation and search. Constraint solvers are complex programs, and many existing and widely used CLP(FD) systems suffer from limitations and mistakes that can cause them to miss valid solutions or give wrong answers. In this thesis, we show examples of common limitations and mistakes of several widely used CLP(FD) systems. We then present a new CLP(FD) system that overcomes some of these issues. Our system has several unique features such as monotonicity, reasoning over arbitrarily large integers and always terminating propagation. This yields new application opportunities for constraint solvers which we also present. We develop new domain-specific languages that let us concisely and declaratively express parts of our system whose encoding would otherwise be difficult and error prone, such as parsing, propagator selection and constraint reification. We present two methods for testing our solver: systematic test cases, and automated analysis of individual propagators. Our contributions are applicable to other constraint systems as well and may improve their correctness.