Algorithm to detect and remove least number of inconsistent facts (probably in PROLOG)?

Question

How do you program the following algorithm?

Imagine a list of "facts" like this, where the letters represent variables bound to numeric values:

x = 1
y = 2
z = 3
a = 1
b = 2
c = 3
a = x
b = z
c = z

These "facts" clearly must not all be "true": it's not possible for b=z while b=2 and z=3. If either b=z or b=2 were removed, all facts would be consistent. If z=3 and either b=z or c=z were removed, then all facts would be consistent but there would be one fewer fact than above. This set contains many such consistent subsets. For instance, a=1, b=2, c=3 is a consistent subset, and so are many others.

Two consistent subsets are larger than any other consistent subset in this example:

x = 1
y = 2
z = 3
a = 1
b = 2
c = 3
a = x
c = z

and

x = 1
y = 2
z = 3
a = 1
c = 3
a = x
b = z
c = z

Using an appropriate programming language (I'm thinking PROLOG, but maybe I'm wrong) how would you process a large set containing consistent and inconsistent facts, and then output the largest possible sub-set of consistent facts (or multiple subsets as in the example above)?

Answer 1

This is very closely related to the NP-hard multiway cut problem. In the (unweighted) multiway cut problem, we have an undirected graph and a set of terminal vertices. The goal is to remove as few edges as possible so that each terminal vertex lies in its own connected component.

For this problem, we can interpret each variable and each constant as a vertex, and each equality as an edge from its left-hand side to its right-hand side. The terminal vertices are those associated with constants.

For only two terminals, the multiway cut problem is the polynomial-time solvable s-t minimum cut problem. We can use minimum cuts to get a polynomial-time 2-approximation to the multiway cut problem, by finding the cheapest cut separating two terminals, deleting the edges involved, and then recursing on the remaining connected components. Several approximation algorithms with better ratios have been proposed in the theoretical literature on multiway cut.

Practically speaking, multiway cut arises in applications to computer vision, so I would expect that there has been some work on obtaining exact solutions. I don't know what's out there, though.