Dimacs cnf expression not satisfiable, why?

Question

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?

Answer 1

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.