As an amusing example, consider the Pigeonhole Principle, which says that n+1 pigeons can’t be placed into n holes, with at most one pigeon per hole. It’s not hard to construct a propositional Boolean formula Φ that encodes the Pigeonhole Principle for some fixed value of n (say, 1000). However, if you then feed Φ to current Boolean satisfiability algorithms, they’ll assiduously set to work trying out possibilities: “let’s see, if I put this pigeon here, and that one there … darn, it still doesn’t work!” And they’ll continue trying out possibilities for an exponential number of steps, oblivious to the “global” reason why the goal can never be achieved. Indeed, beginning in the 1980s, the field of proof complexity—a close cousin of computational complexity—has been able to show that large classes of algorithms require exponential time to prove the Pigeonhole Principle and similar propositional tautologies.
Hmm. The simplex method would determine that this is infeasible in at most n steps, so I’m not sure how generalizable this result is.
(Beyond that, it seems to me that this should be solvable in one step, by assuming what you want to prove and checking for contradictions. You convert “at most one” to “one”, figure out that the largest feasible number of pigeons is 1,000, which is less than 1,001 and you’re done. This looks like it depends on the symmetry of the problem, though, and so for general problems you’d need to use simplex.)
I’ve been thinking about this again recently, and I think I can articulate better what I was thinking then.
The Pigeonhole Principle is an example of a Boolean satisfiability problem that smells like an optimization problem. If you convert the problem to “fit as many pigeons into holes as possible,” you can determine the maximum number of pigeons in linear time with respect to the number of constraints, and then compare the maximum number of pigeons to n+1, you discover than n+1 is going to be greater than n.
There’s no guarantee that you can recast a general Boolean satisfiability problem as an optimization problem- but I suspect that if it’s “obvious” to human observers that a propositional Boolean formula will be true or untrue, it’s because you can recast that problem as an optimization problem. The Boolean satisfiability algorithms that take an exponential number of steps do so because they’re designed to be able to solve any problem, rather than get the right answer quickly to a limited class of problems. That is, the simplex method is irrelevant to Boolean satisfiability in general but is very relevant to the class of problems that humans can see the answer to and Boolean satisfiability algorithms founder on.
Sure, in that it can’t solve all boolean satisfiability problems. I understood the section as saying “look, these methods don’t apply heuristics and so can spend an inordinate amount of time proving things that are trivial if you use heuristics,” and so gave an example of an optimization method which won’t use an inordinate amount of time to determine infeasibility, and is stronger / more useful than human intuition in the domains where it can be applied.
Hmm. The simplex method would determine that this is infeasible in at most n steps, so I’m not sure how generalizable this result is.
(Beyond that, it seems to me that this should be solvable in one step, by assuming what you want to prove and checking for contradictions. You convert “at most one” to “one”, figure out that the largest feasible number of pigeons is 1,000, which is less than 1,001 and you’re done. This looks like it depends on the symmetry of the problem, though, and so for general problems you’d need to use simplex.)
The simplex method is irrelevant to boolean satisfiability.
I’ve been thinking about this again recently, and I think I can articulate better what I was thinking then.
The Pigeonhole Principle is an example of a Boolean satisfiability problem that smells like an optimization problem. If you convert the problem to “fit as many pigeons into holes as possible,” you can determine the maximum number of pigeons in linear time with respect to the number of constraints, and then compare the maximum number of pigeons to n+1, you discover than n+1 is going to be greater than n.
There’s no guarantee that you can recast a general Boolean satisfiability problem as an optimization problem- but I suspect that if it’s “obvious” to human observers that a propositional Boolean formula will be true or untrue, it’s because you can recast that problem as an optimization problem. The Boolean satisfiability algorithms that take an exponential number of steps do so because they’re designed to be able to solve any problem, rather than get the right answer quickly to a limited class of problems. That is, the simplex method is irrelevant to Boolean satisfiability in general but is very relevant to the class of problems that humans can see the answer to and Boolean satisfiability algorithms founder on.
Sure, in that it can’t solve all boolean satisfiability problems. I understood the section as saying “look, these methods don’t apply heuristics and so can spend an inordinate amount of time proving things that are trivial if you use heuristics,” and so gave an example of an optimization method which won’t use an inordinate amount of time to determine infeasibility, and is stronger / more useful than human intuition in the domains where it can be applied.