patternMinor
Why do we care about random Boolean SAT formula?
Viewed 0 times
randomsatwhybooleancareaboutformula
Problem
I've been looking for a reference for the above question.
As far as I know the answer is:
If we can make a solver that is efficient for all randomly generated instances, it should be efficient for any instance.
i.e. if we make a solver that doesnt rely on any inherent structure, it will always be efficient.
Is this correct? Either way, does anyone have a reference to a paper I can cite for the answer.
As far as I know the answer is:
If we can make a solver that is efficient for all randomly generated instances, it should be efficient for any instance.
i.e. if we make a solver that doesnt rely on any inherent structure, it will always be efficient.
Is this correct? Either way, does anyone have a reference to a paper I can cite for the answer.
Solution
If your solver is efficient for random 3-SAT, it by no means entails that it is efficient for an arbitrary 3-SAT instance. Randomly generated instances are very different from instances that arise in practice (meaning they are structured differently). For instance, you can read about the phase transition in random $k$-SAT: depending on the clause-to-variable ratio, an instance can be easy (not constrained enough, or too constrained) or hard (in some sense critically constrained). This phenomenon is rather fascinating in itself.
You can always argue that if you have a solver that does not exploit any structure of the input and is always rather magically efficient, much of the theory we have developed around SAT is useless. Unfortunately, many people have worked a lot on the problem, and we are still unable to give an efficient algorithm for e.g. SAT (not to mention an algorithm that would be efficient in practice as well!). So how do we cope with this? We look at e.g. structural aspects of the input: what can we leverage? How can we be fast at least sometimes? Because we can't solve a problem we care about, we look for other approaches and angles of attack.
I think the main reasons we have been interested in random $k$-SAT is that first, such instances are easy to generate to test our solvers. We have also learned that random instances are very different from instances that arise in practice (and of course those are the instances we often care about). This has increased our understanding of the nature of computation, heuristics, complexity, and ultimately made us able to build faster solvers as well.
You can always argue that if you have a solver that does not exploit any structure of the input and is always rather magically efficient, much of the theory we have developed around SAT is useless. Unfortunately, many people have worked a lot on the problem, and we are still unable to give an efficient algorithm for e.g. SAT (not to mention an algorithm that would be efficient in practice as well!). So how do we cope with this? We look at e.g. structural aspects of the input: what can we leverage? How can we be fast at least sometimes? Because we can't solve a problem we care about, we look for other approaches and angles of attack.
I think the main reasons we have been interested in random $k$-SAT is that first, such instances are easy to generate to test our solvers. We have also learned that random instances are very different from instances that arise in practice (and of course those are the instances we often care about). This has increased our understanding of the nature of computation, heuristics, complexity, and ultimately made us able to build faster solvers as well.
Context
StackExchange Computer Science Q#37186, answer score: 9
Revisions (0)
No revisions yet.