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...
| Main Authors: | , |
|---|---|
| Format: | Report |
| Published: |
DCS‚ University of Oxford
2011
|