A solver for quantified Boolean and linear constraints

Abstract. We make a number of contributions to the understanding and practical resolution of quantified constraints. Unlike previous work in the CP literature that was essentially focused on constraints expressed as binary tables, we focus on Presburger Arithmetics, i.e., Boolean combinations of linear constraints. We explain why we think this language is especially interesting. From a theoretical perspective, we clarify the problem of the treatment of universal quantifiers by proposing a “symmetric” version of the notion of quantified consistency. This notion imposes to maintain two constraint stores, which will be used to reason on universal and existential variables, respectively. We then describe an implementation of a branch & bound algorithm that integrates both forms of propagation and that is, to the best of our knowledge, the first implementation of a CP solver for this class of quantified constraints.