= Minimal Diagnosis =

<<TableOfContents>>

== 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 {{{edge(u,v)}}}, {{{obs_elabel(u,v,s)}}}, and f(u) = s hold. 
 - If f(v) = m, then {{{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.

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 ==

== Output format ==

== 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). <<BR>>
obs_elabel(0,1,p). obs_elabel(0,3,m). obs_elabel(0,4,m). <<BR>>

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).
}}}
== Author(s) ==
 * Author: Martin Gebser
   * Affiliation: University of Potsdam