No Cover Image

Journal article 1093 views

Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.

Oliver Kullmann Orcid Logo

Fundamenta Informaticae, Volume: 109, Issue: 1, Pages: 83 - 119

Swansea University Author: Oliver Kullmann Orcid Logo

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

DOI (Published version): 10.3233/FI-2011-429

Abstract

Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get...

Full description

Published in: Fundamenta Informaticae
Published: 2011
URI: https://cronfa.swan.ac.uk/Record/cronfa5284
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:52:11Z
last_indexed 2018-02-09T04:31:28Z
id cronfa5284
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T14:54:15.2413571</datestamp><bib-version>v2</bib-version><id>5284</id><entry>2012-02-23</entry><title>Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.</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-02-23</date><deptcode>SCS</deptcode><abstract>Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or &#x201C;encoding&#x201D;) of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the &#x201C;generic translation scheme&#x201D;.</abstract><type>Journal Article</type><journal>Fundamenta Informaticae</journal><volume>109</volume><journalNumber>1</journalNumber><paginationStart>83</paginationStart><paginationEnd>119</paginationEnd><publisher/><placeOfPublication/><issnPrint/><issnElectronic/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2011</publishedYear><publishedDate>2011-12-31</publishedDate><doi>10.3233/FI-2011-429</doi><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T14:54:15.2413571</lastEdited><Created>2012-02-23T17:01:57.0000000</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></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T14:54:15.2413571 v2 5284 2012-02-23 Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure. 2b410f26f9324d6b06c2b98f67362d05 0000-0003-3021-0095 Oliver Kullmann Oliver Kullmann true false 2012-02-23 SCS Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or “encoding”) of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the “generic translation scheme”. Journal Article Fundamenta Informaticae 109 1 83 119 31 12 2011 2011-12-31 10.3233/FI-2011-429 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2013-10-17T14:54:15.2413571 2012-02-23T17:01:57.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Oliver Kullmann 0000-0003-3021-0095 1
title Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
spellingShingle Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
Oliver Kullmann
title_short Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
title_full Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
title_fullStr Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
title_full_unstemmed Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
title_sort Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure.
author_id_str_mv 2b410f26f9324d6b06c2b98f67362d05
author_id_fullname_str_mv 2b410f26f9324d6b06c2b98f67362d05_***_Oliver Kullmann
author Oliver Kullmann
author2 Oliver Kullmann
format Journal article
container_title Fundamenta Informaticae
container_volume 109
container_issue 1
container_start_page 83
publishDate 2011
institution Swansea University
doi_str_mv 10.3233/FI-2011-429
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 Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or “encoding”) of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the “generic translation scheme”.
published_date 2011-12-31T03:06:20Z
_version_ 1763749690398998528
score 11.014067

Similar Items