\documentclass{article}
\begin{document}
Constraint Satisfaction Problems (CSP) are commonly found in practice and finding effective representation language and efficient constraint solving techniques are important research areas. A recent development is the integration of CSP (specifically SAT) solvers with relational database systems to enable CSPs to be modelled using SQL, and solved within the database system.  A key challenge in this integration is to keep the SAT encoding of SQL constraints small.  In this work, we describe a divide-and- conquer technique for reducing the encoding of cardinality constraints.  We present a number of experiments to show the improvements on performance.
\end{document}