Local consistency and SAT−solvers
Local consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint satisfaction problem is precisely captured by using a particular inference rule,...
| Main Authors: | , |
|---|---|
| Formato: | Journal article |
| Publicado em: |
2012
|
| _version_ | 1826301252138434560 |
|---|---|
| author | Jeavons, P Petke, J |
| author_facet | Jeavons, P Petke, J |
| author_sort | Jeavons, P |
| collection | OXFORD |
| description | Local consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint satisfaction problem is precisely captured by using a particular inference rule, which we call negative-hyper-resolution, on the standard direct encoding of the problem into Boolean clauses. We also show that current clause-learning SAT-solvers will discover in expected polynomial time any inconsistency that can be deduced from a given set of clauses using negative-hyper-resolvents of a fixed size. We combine these two results to show that, without being explicitly designed to do so, current clause-learning SAT-solvers efficiently simulate k-consistency techniques, for all fixed values of k. We then give some experimental results to show that this feature allows clause-learning SAT-solvers to efficiently solve certain families of constraint problems which are challenging for conventional constraint-programming solvers. |
| first_indexed | 2024-03-07T05:29:35Z |
| format | Journal article |
| id | oxford-uuid:e1c6261f-2128-4332-ad8f-cd0b80e88fbb |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:29:35Z |
| publishDate | 2012 |
| record_format | dspace |
| spelling | oxford-uuid:e1c6261f-2128-4332-ad8f-cd0b80e88fbb2022-03-27T09:56:37ZLocal consistency and SAT−solversJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e1c6261f-2128-4332-ad8f-cd0b80e88fbbDepartment of Computer Science2012Jeavons, PPetke, JLocal consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint satisfaction problem is precisely captured by using a particular inference rule, which we call negative-hyper-resolution, on the standard direct encoding of the problem into Boolean clauses. We also show that current clause-learning SAT-solvers will discover in expected polynomial time any inconsistency that can be deduced from a given set of clauses using negative-hyper-resolvents of a fixed size. We combine these two results to show that, without being explicitly designed to do so, current clause-learning SAT-solvers efficiently simulate k-consistency techniques, for all fixed values of k. We then give some experimental results to show that this feature allows clause-learning SAT-solvers to efficiently solve certain families of constraint problems which are challenging for conventional constraint-programming solvers. |
| spellingShingle | Jeavons, P Petke, J Local consistency and SAT−solvers |
| title | Local consistency and SAT−solvers |
| title_full | Local consistency and SAT−solvers |
| title_fullStr | Local consistency and SAT−solvers |
| title_full_unstemmed | Local consistency and SAT−solvers |
| title_short | Local consistency and SAT−solvers |
| title_sort | local consistency and sat solvers |
| work_keys_str_mv | AT jeavonsp localconsistencyandsatsolvers AT petkej localconsistencyandsatsolvers |