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...
| Autori principali: | , |
|---|---|
| Natura: | Report |
| Pubblicazione: |
DCS‚ University of Oxford
2011
|
| _version_ | 1826264665635684352 |
|---|---|
| author | Petke, J Jeavons, P |
| author_facet | Petke, J Jeavons, P |
| author_sort | Petke, J |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T20:11:30Z |
| format | Report |
| id | oxford-uuid:2ab6a7b7-1ec1-416f-962e-eb3553b0f687 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:11:30Z |
| publishDate | 2011 |
| publisher | DCS‚ University of Oxford |
| record_format | dspace |
| spelling | oxford-uuid:2ab6a7b7-1ec1-416f-962e-eb3553b0f6872022-03-26T12:26:38ZThe order encoding: from tractable CSP to tractable SATReporthttp://purl.org/coar/resource_type/c_93fcuuid:2ab6a7b7-1ec1-416f-962e-eb3553b0f687Department of Computer ScienceDCS‚ University of Oxford2011Petke, JJeavons, PMany 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. |
| spellingShingle | Petke, J Jeavons, P The order encoding: from tractable CSP to tractable SAT |
| title | The order encoding: from tractable CSP to tractable SAT |
| title_full | The order encoding: from tractable CSP to tractable SAT |
| title_fullStr | The order encoding: from tractable CSP to tractable SAT |
| title_full_unstemmed | The order encoding: from tractable CSP to tractable SAT |
| title_short | The order encoding: from tractable CSP to tractable SAT |
| title_sort | order encoding from tractable csp to tractable sat |
| work_keys_str_mv | AT petkej theorderencodingfromtractablecsptotractablesat AT jeavonsp theorderencodingfromtractablecsptotractablesat AT petkej orderencodingfromtractablecsptotractablesat AT jeavonsp orderencodingfromtractablecsptotractablesat |