This file is from Wikimedia Commons and may be used by other projects.
The description on its file description page there is shown below.
Detailed description
This graph is formed from the 2-satisfiability instance
(
x
0
∨
x
2
)
∧
(
x
0
∨
¬
x
3
)
∧
(
x
1
∨
¬
x
3
)
∧
(
x
1
∨
¬
x
4
)
∧
(
x
2
∨
¬
x
4
)
∧
(
x
0
∨
¬
x
5
)
∧
(
x
1
∨
¬
x
5
)
∧
(
x
2
∨
¬
x
5
)
∧
(
x
3
∨
x
6
)
∧
(
x
4
∨
x
6
)
∧
(
x
5
∨
x
6
)
{\displaystyle \scriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \scriptstyle \quad (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6})}
by replacing each disjunction by the two implications to which it is equivalent, e.g.,
(
x
0
∨
¬
x
3
)
≡
(
¬
x
0
⇒
¬
x
3
)
≡
(
x
3
⇒
x
0
)
,
{\displaystyle \scriptstyle (x_{0}\lor \lnot x_{3})\equiv (\lnot x_{0}\Rightarrow \lnot x_{3})\equiv (x_{3}\Rightarrow x_{0}),}
and then representing the implications graphically as directed edges in a graph.
The solution set for the same example instance is depicted in Image:2SAT median graph.svg .
English Add a one-line explanation of what this file represents
File history
Click on a date/time to view the file as it appeared at that time.
Date/Time Thumbnail Dimensions User Comment
current 20:41, 29 November 2008 612 × 504 (10 KB) wikimediacommons>David Eppstein Fix ~x6 vertex in new drawing
File usage
The following 3 pages use this file: