ciphergoth: what's ISTR?

**Linear Algebra as a Reasoning Technique**

Consider a problem statement with some number of boolean variables, and restraints along the lines of 'out of this assignment, at least x must be true'. For example, in a problem with five variables, you might have a constraint stating 'of a, b, not c, not d, and e, at least three must be true'.

We can construct a linear relaxation of this problem by replacing boolean variables with numbers in the range [0, 1] and replacing their constrains with linear constraints, for example the above clause would change to a + b + (1 - c) + (1 - d) + e >= 3.

This allows us to do a very interesting trick. Pick a random assignment to all the variables, and calculate the minimum number of them which can be true (their sum) in the linear relaxation. If the values which generate that result round off to a satisfying assignment, we're done. If not, we can take the minimum value, say it's 2.5, and deduce that since each of the values is 0 or 1, the minimum must be the next higher integer, in this case 3. We can then express this as a new linear constraint and add it to the list of constraints. If we do this repeatedly, we may nail down the constraints enough to force the approximation we find to yield an actual solution or show that none exists.

I should emphasize that this is a *reasoning* method and not an *approximation* method. If this technique keeps adding constraints until there is no solution to the linear relaxation, that constitutes a formal proof that the original boolean problem has no solution. My motivation in coming up with this technique is that all exhaustive techniques for NP-complete problems I've heard of are backtracking algorithms, and I'm trying to find an exception to that rule.

If the minimum values given in the constraints are less than half the number of variables in them, then the linear relaxation can always be solved by setting all values to 1/2, and the round-up trick won't be able to get past that point. This is why this technique doesn't work for basic SAT problems. Yeah that's obvious, but it took me a few years to realize, and I haven't had access to a decent linear programming package since then, so I don't know for sure that this technique is effective on the more appropriate problems I've suggested, although it seems promising.

Hard instances of these problems can probably be generated simply by adding new random constraints until it gets to the point where there's a 50% chance of there being a solution, at which point both finding any solution and determining that there isn't one by backtracking will be hard.