# Minimal Diagnosis

## Problem Description

This problem is motivated by an existing application in systems biology, described here: http://www.cs.uni-potsdam.de/wv/pdfformat/gescthve10a.pdf

The input is an influence graph provided in terms of facts of the form:

vertex(0). ... vertex(n). input(i_0). ... input(i_m). obs_vlabel(v_0,l_0). ... obs_vlabel(v_j,l_j). edge(e_0,e_1). ... edge(e_{k-1},e_k). obs_elabel(e_0,e_1,s_(0,1)). ... obs_elabel(e_{k-1},e_k,s_(k-1,k)).

The facts over vertex/1 include consecutive integers in [0,n] as the names of vertices. The values of the following arguments of other facts are also in [0,n]:

i_0,...,i_m, v_0,...,v_j, e_0,...,e_k.

The following vertex labels or edge labels, respectively, are either "p" or "m" each:

l_0,...,l_j, s_(0,1),...,s_(k-1,k).

A total labeling of vertices is a total function f : [0,n] -> {p,m} such that f(v_{i}) = l_{i} if a fact `obs_vlabel(v_i,l_i)` belongs to the input.

The labeling f is consistent for a vertex v in [0,n] if the following holds:

If f(v) = p, then there is some u in [0,n] for which

`edge(u,v)`,`obs_elabel(u,v,s)`, and f(u) = s hold.If f(v) = m, then there is some u in [0,n] for which

`edge(u,v)`,`obs_elabel(u,v,s)`, and f(u) = t hold such that s is different from t.

A Minimal Inconsistent Core M is a subset of [0,n] \ {i_{0},...,i_{m}} such that:

- There is no total labeling f that is consistent for every vertex v in M.
- For every proper subset N of M, there is some total labeling f that is consistent for every vertex v in N.

Note that vertices in the relation expressed by predicate `input/1` cannot belong to a Minimal Inconsistent Core.

A solution, i.e., a Minimal Inconsistent Core is represented by instances of active/1: `active(v)`.

The vertices v for which `active(v)` holds must form a Minimal Inconsistent Core for the given input.

Verifying whether a given set of vertices is a Minimal Inconsistent Core is D^{P}-complete, cf.:

Papadimitriou, C. and Yannakakis, M. 1982. The complexity of facets (and some facets of complexity). Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC’82). ACM Press, 255–260.

## Predicates

**Input**:`edge/2, input/1, obs_elabel/3, obs_vlabel/2, vertex/1`**Output**:`active/1`

## Input format

Vertices of the input graph are specified by means of predicate `vertex/1`. More specifically, if the graph has `n` vertices, the input comprises `n+1` facts of the form `vertex(i)`, where `i = 0, ..., n`.

A set of vertices that cannot belong to a Minimal Inconsistent Core is specified by means of predicate `input/1`.

Edges of the input graph are specified by means of predicate `edge/2`.

A partial labeling of vertices is specified by means of predicate `obs_vlabel/2`, where the first argument is a vertex index (an integer between 0 and n), and the second argument is either `p` or `m`.

A total labeling of edges is specified by means of predicate `obs_elabel/3`, where the first two arguments represent an edge, and the third argument is either `p` or `m`.

## Output format

A Minimal Inconsistent Core represented by means of predicate `active/1`. More specifically, the output should comprise facts of the form `active(v)` whenever the vertex `v` is part of the Minimal Inconsistent Core.

## Example(s)

Consider the following input:

vertex(0). vertex(1). vertex(2). vertex(3). vertex(4). obs_vlabel(1,p). obs_vlabel(3,p). edge(0,1). edge(0,3). edge(0,4). obs_elabel(0,1,p). obs_elabel(0,3,m). obs_elabel(0,4,m). edge(1,0). obs_elabel(1,0,p). edge(1,2). obs_elabel(1,2,p). edge(2,4). obs_elabel(2,4,m). edge(3,1). edge(3,2). edge(3,4). obs_elabel(3,1,p). obs_elabel(3,2,p). obs_elabel(3,4,p).

The only Minimal Inconsistent Core contains the vertices 0 and 3. It is represented by:

active(0). active(3).

Example Figure:

Additional sample instances: download

## Problem Peculiarities

**Type**: Search **Competition**: System Track

## Notes and Updates

## Author(s)

- Author: Marcello Balduccini
- Affiliation: Kodak Research Labs

- Original Author: Martin Gebser
- Affiliation: University of Potsdam, Germany