The order encoding: from tractable CSP to tractable SAT

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...

Full description

Bibliographic Details
Main Authors: Petke, J, Jeavons, P
Format: Report
Published: DCS‚ University of Oxford 2011