Encoding quadratic constraints in a constraint satisfaction problem into SAT

Question

It seems like most constraint satisfaction problems can be posed in terms of SAT.

The question is two fold:

1. How can any CSP with quadratic constraints be framed as a satisfiability instance
2. Is there an algorithm which performs this transformation.

Answer 1

This of course depends on the type of satisfaction problems you are trying you encode in SAT. Assuming the general case, where your problem falls into the class of problems that can be handled by some existing encoding techniques (a review of some techniques can be found in [1]), some techniques are specific to support encoding quadratic constraints (and arithmetic operations such as multiplication, in general):

1) Some of the approaches for encoding quadratic constraints, as well as other form of constraints that involve arithmetic operations, into SAT include encoding techniques often referred to as 'bit blasting' or such as the ones based on sparse encoding:

• Bit blasting is a commonly used decision procedure for bit-vector arithmetic. Essentially, the idea is to represent bit-vector terms with vector of Boolean variables and emit constraints on the bits of those vectors depending on the constants and operations used in the formula, where arithmetic operations are encoded as "circuits", which effectively put constraints for every bit of the resulting vector. (More information about this technique can be found e.g. in [2]).
• Sparse encoding (of integers) is an approach, interestingly different from bit blasting, which avoids using circuits by trying to precompute possible integer values and using guards in the encoding to designate when can a term hold a specific value (depending on the structure of the constraint and possible starting values). Such a technique might be superior to bit blasting for cases of considering smaller integer domains. (More details and the discussion about benefits of using this approach is presented in [3].)

2) There exist different ways of leveraging techniques such as bit blasting and sparse encoding for the purpose of encoding different (CSP) problems into SAT, while some of the mentioned literature directly suggests plausible algorithms: a standard approach for a translating algorithm is described in [2], while the algorithm that relies on sparse encoding is implemented in a software synthesizer Sketch, and described in detail through examples in [4].

[1] Walsh, Toby. "Sat v csp." International Conference on Principles and Practice of Constraint Programming. Springer Berlin Heidelberg, 2000.

[2] Kroening, Daniel, and Ofer Strichman. Decision procedures: an algorithmic point of view. Springer Science & Business Media, 2008.

[3] Solar-Lezama, Armando. Program synthesis by sketching.

[4] Solar-Lezama, Armando. "Program sketching." International Journal on Software Tools for Technology Transfer 15.5-6 (2013): 475-495.