Journal article 1126 views
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution
Journal of Automated Reasoning, Volume: 52, Issue: 1, Pages: 31 - 65
Swansea University Author:
Oliver Kullmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/s10817-013-9275-8
Abstract
The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fun...
| Published in: | Journal of Automated Reasoning |
|---|---|
| ISSN: | 0168-7433 1573-0670 |
| Published: |
2014
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa13746 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fundamental is the notion of "hardness", which is explored here systematically. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Issue: |
1 |
| Start Page: |
31 |
| End Page: |
65 |