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