No Cover Image

Journal article 406 views

Constraint satisfaction problems in clausal form I: Autarkies and deficiency. / Oliver, Kullmann

Fundamenta Informaticae, Volume: 109, Issue: 1, Pages: 27 - 81

Swansea University Author: Oliver, Kullmann

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

Check full text

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

Abstract

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals...

Full description

Published in: Fundamenta Informaticae
ISSN: 0169-2968
Published: 2011
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa5283
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals”, corresponding to unary constraints in CSP. However we argue that only the restricted form of “negative monosigned literals” and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency.
College: College of Science
Issue: 1
Start Page: 27
End Page: 81