Unsatisfying

This problem gives us a series of boolean disjunctions of size 2 and asks us how many more do we have to add to make the expression unsatisfiable. The only condition is the added disjunctions can not use negation.

One can clearly see this is related to 2-SAT, and so one must know the 2 sat algorithm, namely to create a graph of each literal and its negation. Draw an edge from each literal in any disjunction to the inverse of the literal it is paired with in that disjunction. One can then see if the expression is unsatisfiable if any strongly connected component contains a literal and its negation. This makes sense as it means x->not x, and not x-> x, which means neither value will work.

Assuming the given expression has no solution (else the solution is trivial!), we know there are no strongly connected components of the above form. To make it unsatisfiable, we must create one.

The restriction on the form of the added disjunctions means that any edge we draw will always go from not(something) -> something. Not only that, but it means we can link ANY negative literal to ANY positive literal. This limits our maximum answer to TWO. Why? Suppose the minimum answer was three. Since we cannot connect two added disjunctions together (since the edges only go negative->positive), this means we connect three currently unconnected components to ensure the newly strongly connected component contains some literal and its negation. However, this means one of the three previously unconnected components contained neither that literal or its negation. Given that is the case, we could have connected the other two components which did contain the literals directly without the third one. This takes 2 disjunctions at most.

So now we just have to decide whether to do it with 2 or 1.

1) there is some component containing both x and !x (for some x). There is some negative literal which is descendent of both of these, and some positive literal which is an ancestor, we can add a single disjunction that goes from the negative to the positive literal. 2) there are separate components containing x and !x. x has some descendent literal which is negative, and !x has the same literal, but positive, as an ancestor, and vice versa. We can do it with 1. 2) there are separate components containing x and !x. x has a negative descendent, and !x has a positive ancestor, we can do it with 2

We can try this for all x and take the minimum. Each one takes linear time, and 2000^2 is fast enough.