No Cover Image

Journal article 1485 views

On Davis–Putnam reductions for minimally unsatisfiable clause-sets

Oliver Kullmann Orcid Logo, Xishun Zhao

Theoretical Computer Science, Volume: 492, Pages: 70 - 87

Swansea University Author: Oliver Kullmann Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

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...

Full description

Published in: Theoretical Computer Science
ISSN: 0304-3975
Published: 2013
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa13745
first_indexed 2013-07-23T12:10:50Z
last_indexed 2019-06-05T09:30:43Z
id cronfa13745
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-06-04T14:18:02.7292382</datestamp><bib-version>v2</bib-version><id>13745</id><entry>2012-12-17</entry><title>On Davis&#x2013;Putnam reductions for minimally unsatisfiable clause-sets</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>MACS</deptcode><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.</abstract><type>Journal Article</type><journal>Theoretical Computer Science</journal><volume>492</volume><paginationStart>70</paginationStart><paginationEnd>87</paginationEnd><publisher/><issnPrint>0304-3975</issnPrint><keywords/><publishedDay>24</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2013</publishedYear><publishedDate>2013-06-24</publishedDate><doi>10.1016/j.tcs.2013.04.020</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-06-04T14:18:02.7292382</lastEdited><Created>2012-12-17T21:33:45.5804053</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>Oliver</firstname><surname>Kullmann</surname><orcid>0000-0003-3021-0095</orcid><order>1</order></author><author><firstname>Xishun</firstname><surname>Zhao</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2019-06-04T14:18:02.7292382 v2 13745 2012-12-17 On Davis–Putnam reductions for minimally unsatisfiable clause-sets 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2012-12-17 MACS "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. Journal Article Theoretical Computer Science 492 70 87 0304-3975 24 6 2013 2013-06-24 10.1016/j.tcs.2013.04.020 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2019-06-04T14:18:02.7292382 2012-12-17T21:33:45.5804053 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Oliver Kullmann 0000-0003-3021-0095 1 Xishun Zhao 2
title On Davis–Putnam reductions for minimally unsatisfiable clause-sets
spellingShingle On Davis–Putnam reductions for minimally unsatisfiable clause-sets
Oliver Kullmann
title_short On Davis–Putnam reductions for minimally unsatisfiable clause-sets
title_full On Davis–Putnam reductions for minimally unsatisfiable clause-sets
title_fullStr On Davis–Putnam reductions for minimally unsatisfiable clause-sets
title_full_unstemmed On Davis–Putnam reductions for minimally unsatisfiable clause-sets
title_sort On Davis–Putnam reductions for minimally unsatisfiable clause-sets
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Oliver Kullmann
Xishun Zhao
format Journal article
container_title Theoretical Computer Science
container_volume 492
container_start_page 70
publishDate 2013
institution Swansea University
issn 0304-3975
doi_str_mv 10.1016/j.tcs.2013.04.020
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
document_store_str 0
active_str 0
description "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.
published_date 2013-06-24T04:22:38Z
_version_ 1850821951344345088
score 11.088929

Similar Items