File:Schaefer's dichotomy theorem relation hierarchy.gif

Uploaded by Jochen Burghardt
Upload date 2017-11-22T14:22:00Z
MIME type image/gif
Dimensions 797 × 520 px
File size 12.8 KB

Summary

Description
English: This Hasse diagram shows all ternary relations R on Boolean values that are invariant to argument permutation, i.e. such that R(x1,x2,x3) holds iff R(xσ(1),xσ(2),xσ(3)) holds, for every permutation σ of the set {1,2,3}; in order to determine if R holds on a triple it is sufficient to know the count of its true values.

An arrow from R1 upwards to R2 indicates that R1(x1,x2,x3) implies R2(x1,x2,x3). The set ot true-argument counts for which a relation holds is shown in the left of each node, while the right shows some mnemonic (nor: negated or, ae: all equal, maj: majority, min: minority, eqv: equivalence, nae: not all equal, n2in3: not exactly 2 arguments are true, n1in3: not exactly 1 argument is true, nand: negated and). The formal definition of all 16 relations is given by the table below.

According to Schaefer's dichotomy theorem, the problem of deciding the satisfiability of a generalized conjunctive normal form is either NP complete or in P, depending on the relation R employed to form generalized clauses. Correspondingly, the node of R is colored red and green, respectively.

Some particular cases that are discussed in more detail in English Wikipedia articles are linked via image annotations.

For the NP-complete relations, the reduction of or to each of them is shown below. For each combination of X, Y, Z, the relation or(X,Y,Z) holds iff appropriate values of the auxiliary variables a,...,d exist such that the reduction formula on the right-hand side holds. The reduction formulas are the shortest ones that were found by a brute-force search.

Date
Source Own work
Author Jochen Burghardt
Formal definition of the used ternary relations
cnt x y z false and nor 2in3 1in3 ae xor maj min eqv nae n2in3 n1in3 or nand true
0 f f f f f t f f t f f t t f t t f t t
1 f f t f f f f t f t f t f t t f t t t
1 f t f f f f f t f t f t f t t f t t t
2 f t t f f f t f f f f f t t f t t t t
1 t f f f f f f t f t f t f t t f t t t
2 t f t f f f t f f f f f t t f t t t t
2 t t f f f f t f f f f f t t f t t t t
3 t t t f t f f f t t t f f f t t t f t
Reductions of or to 2in3, 1in3, nae, n2in3, n1in3, nand
or( X, Y, Z) equi-satisfiable 2in3( X, a, b) 2in3( Y, c, d) 2in3( ¬Z, a, c)
0 0 0 0 0 0 1
1 1 0 0 1 1 0 1 1 0 1 1 1 1 0 1
1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 0
1 1 1 0 1 1 0 1 1 1 1 0 1 1 0 1
1 0 0 1 1 0 1 1 1 0 1 1 1 0 1 1
1 1 0 1 1 1 1 0 1 0 1 1 1 0 1 1
1 0 1 1 1 0 1 1 1 1 1 0 1 0 1 1
1 1 1 1 1 1 1 0 1 1 1 0 1 0 1 1
or( X, Y, Z) equi-satisfiable 1in3( X, a, b) 1in3( ¬Y, a, c) 1in3( ¬Z, b, d)
0 0 0 0 0 1 1
1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0
1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 0
1 1 1 0 1 1 0 0 1 0 0 1 1 1 0 0
1 0 0 1 1 0 0 1 1 1 0 0 1 0 1 0
1 1 0 1 1 1 0 0 1 1 0 0 1 0 0 1
1 0 1 1 1 0 0 1 1 0 0 1 1 0 1 0
1 1 1 1 1 1 0 0 1 0 0 1 1 0 0 1
or( X, Y, Z) equi-satisfiable nae( 0, X, a) nae( Y, Z, ¬a)
0 0 0 0 0 0 0 0
1 1 0 0 1 0 1 0 1 0 0 1
1 0 1 0 1 0 0 1 1 1 0 0
1 1 1 0 1 0 1 0 1 1 0 1
1 0 0 1 1 0 0 1 1 0 1 0
1 1 0 1 1 0 1 0 1 0 1 1
1 0 1 1 1 0 0 1 1 1 1 0
1 1 1 1 1 0 1 1 1 1 1 0
or( X, Y, Z) equi-satisfiable n2in3( 0, ¬X, a) n2in3( ¬Y, ¬Z, a)
0 0 0 0 0 1 1 1
1 1 0 0 1 0 0 1 1 1 1 1
1 0 1 0 1 0 1 0 1 0 1 0
1 1 1 0 1 0 0 0 1 0 1 0
1 0 0 1 1 0 1 0 1 1 0 0
1 1 0 1 1 0 0 0 1 1 0 0
1 0 1 1 1 0 1 0 1 0 0 0
1 1 1 1 1 0 0 0 1 0 0 0
or( X, Y, Z) equi-satisfiable n1in3( 1, X, a) n1in3( Y, Z, a)
0 0 0 0 1 0 0 0
1 1 0 0 1 1 1 0 1 0 0 0
1 0 1 0 1 1 0 1 1 1 0 1
1 1 1 0 1 1 1 1 1 1 0 1
1 0 0 1 1 1 0 1 1 0 1 1
1 1 0 1 1 1 1 1 1 0 1 1
1 0 1 1 1 1 0 1 1 1 1 1
1 1 1 1 1 1 1 0 1 1 1 0
or( X, Y, Z) equi-satisfiable nand( ¬X, ¬Y, ¬Z)
0 0 0 0 0 1 1 1
1 1 0 0 1 0 1 1
1 0 1 0 1 1 0 1
1 1 1 0 1 0 0 1
1 0 0 1 1 1 1 0
1 1 0 1 1 0 1 0
1 0 1 1 1 1 0 0
1 1 1 1 1 0 0 0


Licensing

I, the copyright holder of this work, hereby publish it under the following license:
w:en:Creative Commons
attribution share alike
This file is licensed under the Creative Commons Attribution-Share Alike 4.0 International license.
You are free:
  • to share – to copy, distribute and transmit the work
  • to remix – to adapt the work
Under the following conditions:
  • attribution – You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
  • share alike – If you remix, transform, or build upon the material, you must distribute your contributions under the same or compatible license as the original.
Annotations
InfoField
This image is annotated: View the annotations at Commons

Captions

Add a one-line explanation of what this file represents

Items portrayed in this file

depicts

22 November 2017

Category:Boolean satisfiability problem Category:CC-BY-SA-4.0 Category:Created with xgraph Category:Files by User:Jochen Burghardt Category:Hasse diagrams Category:Images with annotations Category:Self-published work