Journal article 998 views
On Davis–Putnam reductions for minimally unsatisfiable clause-sets
Oliver Kullmann 
,
Xishun Zhao
,
Xishun Zhao
Theoretical Computer Science, Volume: 492, Pages: 70 - 87
Swansea University Author:
Oliver Kullmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1016/j.tcs.2013.04.020
Abstract
"Minimally unsatisfiable clause-sets" are fundamental building blocks of satisfiability (SAT) theory. In order to establish a structural theory about them,elimination of certain types of degenerations via "Davis-Putnam (DP) reductions" are essential. These DP-reductions have been...
| Published in: | Theoretical Computer Science |
|---|---|
| ISSN: | 0304-3975 |
| Published: |
2013
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa13745 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
"Minimally unsatisfiable clause-sets" are fundamental building blocks of satisfiability (SAT) theory. In order to establish a structural theory about them,elimination of certain types of degenerations via "Davis-Putnam (DP) reductions" are essential. These DP-reductions have been used at many placessince more than 50 years, and we now show that we have certain forms of confluence, that is, that the applications of DP-reductions are independent oftheir implementation, to a certain degree. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Start Page: |
70 |
| End Page: |
87 |