This file is from a shared repository 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 19:41, 29 November 2008 612 × 504 (10 KB) commons>David Eppstein Fix ~x6 vertex in new drawing
File usage
There are no pages that use this file.