It seems like most constraint satisfaction problems can be posed in terms of SAT. The question is two fold:How can any CSP with quadratic constraints be framed as asatisfiability instanceIs there an algorithm which performs thistransformation.
Encoding quadratic constraints in a constraint satisfaction problem into SAT
sat;csp