All reports by Author Oliver Kullmann:

__
TR07-055
| 22nd May 2007
__

Oliver Kullmann#### Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability

Revisions: 1

__
TR00-018
| 16th February 2000
__

Oliver Kullmann#### An application of matroid theory to the SAT problem

__
TR99-041
| 22nd August 1999
__

Oliver Kullmann#### Investigating a general hierarchy of polynomially decidable classes of CNF's based on short tree-like resolution proofs

Revisions: 2

Oliver Kullmann

We consider the next step from boolean conjunctive normal forms to

arbitrary constraint satisfaction problems (with arbitrary constraints), namely "generalised clause-sets" (or "sets of no-goods"), which allow negative literals "v <> e" for variables v and values e --- this level of generality appears to be the right level for ...
more >>>

Oliver Kullmann

A basic property of minimally unsatisfiable clause-sets F is that

c(F) >= n(F) + 1 holds, where c(F) is the number of clauses, and

n(F) the number of variables. Let MUSAT(k) be the class of minimally

unsatisfiable clause-sets F with c(F) <= n(F) + k.

Poly-time decision algorithms are known ... more >>>

Oliver Kullmann

A relativized hierarchy of conjunctive normal forms

is introduced, recognizable and SAT decidable in polynomial

time. The corresponding hardness parameter, the first level

of inclusion in the hierarchy, is studied in detail, admitting

several characterizations, e.g., using pebble games, the space

complexity of (relativized) tree-like ...
more >>>