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:The second
CNF
:The following truth-table shows all
16
combinations: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:
The second form requires additional clauses to prevent the
g1//g3
to be green whileg2//g4
is green and vice versa.Note that both forms do contain redundant clauses:
A useful
CNF
to control a junction could beThis allows/enforces either
g1//g3
org2//g4
but not both.It is not possible to express this as
2-SAT
form.