A Solver for Quantified Boolean and Linear Constraints

Lucas Bordeaux and Lintao Zhang


We make a number of contributions to the understanding and practical resolution of quantified constraints. Unlike previous work in the CP literature which 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 treatement 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 solver which integrates both forms of propagation and which is, to the best of our knowledge, the first implementation of a CP solver for this class of quantified constraints.


Publication typeInproceedings
Published inThe 22nd Annual ACM Symposium on Applied Computing (SAC 2007)
InstitutionMicrosoft Research
AddressSeoul, Korea
> Publications > A Solver for Quantified Boolean and Linear Constraints