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 a satisfiability instance
- Is there an algorithm which performs this transformation.
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this communityIt seems like most constraint satisfaction problems can be posed in terms of SAT.
The question is two fold:
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:
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].
[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.