No Cover Image

Journal article 487 views

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

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

Swansea University Author: Oliver, Kullmann

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!
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 “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”.
College: College of Science
Issue: 1
Start Page: 83
End Page: 119