A Solver for Quantified Boolean and Linear Constraints

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.

sac_2007_qcp.pdf
PDF file

In  The 22nd Annual ACM Symposium on Applied Computing (SAC 2007)

Details

TypeInproceedings
Pages15
NumberMSR-TR-2006-57
InstitutionMicrosoft Research
AddressSeoul, Korea
> Publications > A Solver for Quantified Boolean and Linear Constraints