Journal article 1005 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!
|
first_indexed |
2013-07-23T12:10:50Z |
---|---|
last_indexed |
2019-06-05T09:30:44Z |
id |
cronfa13746 |
recordtype |
SURis |
fullrecord |
<?xml version="1.0"?><rfc1807><datestamp>2019-06-04T14:20:42.5387475</datestamp><bib-version>v2</bib-version><id>13746</id><entry>2012-12-17</entry><title>Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution</title><swanseaauthors><author><sid>2b410f26f9324d6b06c2b98f67362d05</sid><ORCID>0000-0003-3021-0095</ORCID><firstname>Oliver</firstname><surname>Kullmann</surname><name>Oliver Kullmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-12-17</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Journal of Automated Reasoning</journal><volume>52</volume><journalNumber>1</journalNumber><paginationStart>31</paginationStart><paginationEnd>65</paginationEnd><publisher/><issnPrint>0168-7433</issnPrint><issnElectronic>1573-0670</issnElectronic><keywords/><publishedDay>31</publishedDay><publishedMonth>1</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-01-31</publishedDate><doi>10.1007/s10817-013-9275-8</doi><url>http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013</url><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-06-04T14:20:42.5387475</lastEdited><Created>2012-12-17T22:02:07.2000103</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Matthew</firstname><surname>Gwynne</surname><order>1</order></author><author><firstname>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807> |
spelling |
2019-06-04T14:20:42.5387475 v2 13746 2012-12-17 Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2012-12-17 SCS 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. Journal Article Journal of Automated Reasoning 52 1 31 65 0168-7433 1573-0670 31 1 2014 2014-01-31 10.1007/s10817-013-9275-8 http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2019-06-04T14:20:42.5387475 2012-12-17T22:02:07.2000103 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Matthew Gwynne 1 Oliver Kullmann 0000-0003-3021-0095 2 |
title |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
spellingShingle |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution Oliver Kullmann |
title_short |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
title_full |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
title_fullStr |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
title_full_unstemmed |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
title_sort |
Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution |
author_id_str_mv |
2b410f26f9324d6b06c2b98f67362d05 |
author_id_fullname_str_mv |
2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann |
author |
Oliver Kullmann |
author2 |
Matthew Gwynne Oliver Kullmann |
format |
Journal article |
container_title |
Journal of Automated Reasoning |
container_volume |
52 |
container_issue |
1 |
container_start_page |
31 |
publishDate |
2014 |
institution |
Swansea University |
issn |
0168-7433 1573-0670 |
doi_str_mv |
10.1007/s10817-013-9275-8 |
college_str |
Faculty of Science and Engineering |
hierarchytype |
|
hierarchy_top_id |
facultyofscienceandengineering |
hierarchy_top_title |
Faculty of Science and Engineering |
hierarchy_parent_id |
facultyofscienceandengineering |
hierarchy_parent_title |
Faculty of Science and Engineering |
department_str |
School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science |
url |
http://www.cs.swan.ac.uk/~csoliver/papers.html#SLUR2013 |
document_store_str |
0 |
active_str |
0 |
description |
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. |
published_date |
2014-01-31T03:15:43Z |
_version_ |
1763750280616214528 |
score |
11.016235 |