Patmat: efficient reasoning about mutual exclusion

Faster analysis of wide (but relatively flat) class hierarchies
by using a more efficient encoding of mutual exclusion.

The old CNF encoding for mutually exclusive symbols of a domain
added a quadratic number of clauses to the formula to satisfy.

E.g. if a domain has the symbols `a`, `b` and `c` then
the clauses
```
!a \/ !b  /\
!a \/ !c  /\
!b \/ !c
```
were added.

The first line prevents that `a` and `b` are both true at the same time, etc.

There's a simple, more efficient encoding that can be used instead: consider a
comparator circuit in hardware, that checks that out of `n` signals, at most 1
is true. Such a circuit can be built in the form of a sequential counter and
thus requires only 3n-4 additional clauses [1]. A comprehensible comparison of
different encodings can be found in [2].

[1]: http://www.carstensinz.de/papers/CP-2005.pdf
[2]: http://www.wv.inf.tu-dresden.de/Publications/2013/report-13-04.pdf

0 files changed, 0 insertions, 0 deletions