A Solver for Quantified Boolean and Linear Constraints

Lucas Bordeaux and Lintao Zhang

Abstract

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.

Details

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