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.
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.