I am a new cs student and I have a hard time understanding satisfiability fully.
I have made 2 expressions for a SAT solver. Seperately, they are satisfiable, but together they're not. I don't understand it, because i actually thought they meant the same thing.
I wanted to make an expression that would determine which lights can be green green in an intersection without causing collisions.
First expression:
-1 -2 0
-1 -4 0
-2 -1 0
-2 -3 0
-3 -2 0
-3 -4 0
-4 -3 0
-4 -1 0
Satisfiable
Second expression:
1 3 0
3 1 0
2 4 0
4 2 0
Satisfiable
Together:
-1 -2 0
-1 -4 0
-2 -1 0
-2 -3 0
-3 -2 0
-3 -4 0
-4 -3 0
-4 -1 0
1 3 0
3 1 0
2 4 0
4 2 0
Unsatisfiable
Isn't the first expression just implicitly the same thing as the second expression, and if yes, then why is there a conflict when they are both in same expression?
The first CNF
says in language terms:
Don't allow adjacent green lights around the corner to be switched on at the same time
The second CNF
:
Green 1 or green 3 are ON, or both.
Green 2 or green 4 are ON, or both.
The following truth-table shows all 16
combinations:
G1 G2 G3 G4 | CNF1 CNF2
-----------------+--------------
0 0 0 0 | 1 0
0 0 0 1 | 1 0
0 0 1 0 | 1 0
0 0 1 1 | 0 1
0 1 0 0 | 1 0
0 1 0 1 | 1 0
0 1 1 0 | 0 1
0 1 1 1 | 0 1
1 0 0 0 | 1 0
1 0 0 1 | 0 1
1 0 1 0 | 1 0
1 0 1 1 | 0 1
1 1 0 0 | 0 1
1 1 0 1 | 0 1
1 1 1 0 | 0 1
1 1 1 1 | 0 1
From the table, it can be seen that the first form is the inverse of the second form. Therefore, both cannot be satisfied at the same time.
The first form has seven solutions:
All green lights off (blocking all traffic)
4 times: just one green light on (this might ne inefficient)
g1//g3 ON, g2//g4 OFF
g1//g3 OFF, g2//g4 ON
The second form requires additional clauses to prevent the g1//g3
to be green while g2//g4
is green and vice versa.
Note that both forms do contain redundant clauses:
-1 -2 0
-1 -4 0
-2 -1 0 equivalent to -1 -2
-2 -3 0
-3 -2 0 equivalent to -2 -3
-3 -4 0
-4 -3 0 equivalent to -3 -4
-4 -1 0 equivalent to -1 -4
1 3 0
3 1 0 equivalent to 1 3
2 4 0
4 2 0 equivalent to 2 4
A useful CNF
to control a junction could be
3 4 0
2 3 0
1 4 0
1 2 0
-1 -2 -3 -4 0
This allows/enforces either g1//g3
or g2//g4
but not both.
It is not possible to express this as 2-SAT
form.