The order encoding: from tractable CSP to tractable SAT

Abstract

Many mathematical and practical problems can be expressed as CSPs. One way to solve a CSP instance is to encode it into SAT and use a SAT-solver. However, important information about the problem can get lost during the translation stage. Although the general CSP is known to be NP-complete, there are some classes of CSP instances that have been shown to be tractable. These include the classes of CSP instances that contain only max-closed or connected-row-convex constraints. In this paper we show that translating such instances using some common standard encodings results in SAT instances which do not fall into known tractable classes. However, translating such instances using the order encoding results in SAT instances that do fall into known tractable classes.