When a 2SAT problem isn’t actually a 2SAT problem.

by hobbitalastair

Answer: When I get it wrong.

I asserted that I was trying to solve a 2SAT problem for my SSS2 program. I was wrong.

Specifically, the problem I was trying to solve is actually a more general boolean satisfiability problem. I can’t apply Tarjun’s SCC algorithm, which is sad, because I’ve just coded one up. The root of the issue is that I allowed OR statements, which you can not have. At least not how I was doing them.

I discovered this, because I was thinking about how I was going to create the implication graph. I can create an implication graph, but it will not be solvable through apply a SCC algorithm. Here’s an example of why:

‘a’ is a variable. It is true.

‘b’ is also a variable. It is true if all of [‘a’] is true.

Now, in this case, it should work fine. But if I construct an implication graph for the more general instance, then it doesn’t work. The implications are that, if ‘b’ is true, ‘a’ must also be true. And if ‘a’ is false, then ‘b’ must also be false. Which is not enough to run a depth first search on, or a SCC algorithm – at least not how I currently understand it.

The problem lies in the ‘all’ statement. It’s easy to create indeterminate statements using ‘all’ – for instance:

‘a’ is a variable. It is true.

‘b’  is also a variable. It is true if all of [‘a’, ‘c’] is true.

‘c’ is also a variable. It is true if all of [‘a’, ‘b’] is true.

Are both ‘b’ and ‘c’ true? Or are they both false? Without additional inputs, the graph is indeterminate.

I believe that, to avoid this, I’ll have to make sure that the set of operators is not functionally complete.

Or, I might (still) have the wrong end of the stick…