Describing and Measuring the Complexity of SAT encodings for Constraint Programs.

The CO4 language is a Haskell-like language for specifying constraint systems over structured finite domains. A CO4 constraint system is solved by an automatic transformation into a satisfiability problem in propositional logic that is handed to an external SAT solver. We investigate the problem of predicting the size of formulas produced by the CO4 compiler. The goal is to help the programmer in understanding the resource consumption of CO4 on his program. We present a basic cost model, with some experimental data, and discuss ongoing work towards static analysis. It turns out that analysis steps will use constraint systems as well.