3
$\begingroup$

If all NP-complete problems can be converted to 3-SAT problems I had an idea that would not solve the NP problem but might be a practical solution.

What you could do is simply, make a huge table of 3-SAT problems and whether they are solvable or not. Store this on a giant server.

Then it takes less than polynomial time to look at a 3-SAT problem and look it up in a table.

Two questions, for practical purposes, how big a table would be useful? Does such a table already exist?

$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

I think your approach would be completely infeasible and I am sure that no such table exists. The good news is that SAT solvers using clever algorithms and heuristics are able to solve formulas involving thousands of variables with acceptable running times. If you try to estimate how many entries there would be in your table if it contained all formulas with up to 10,000 variables and 1,000,000 symbols, you will see why I say your approach is infeasible.

The moral is that just because a problem is NP-hard does not mean that algorithms to solve that problem are useless in practice.

$\endgroup$
2
  • $\begingroup$ True, but you could probably discount a lot of the more "easier" examples, and just have lookups for the more difficult ones. They did something similar with solving a rubix cube. $\endgroup$
    – zooby
    Dec 22, 2020 at 21:51
  • 1
    $\begingroup$ Yes, but the problem space for the Rubic cube is tiny compared with the problem space that SAT solvers are able to address. I think you need to look into the SAT solving literature. $\endgroup$
    – Rob Arthan
    Dec 22, 2020 at 22:00
0
$\begingroup$

You can't just brute force 3-sat. That would take too much computational resources. I am pretty sure all the computers on earth would not be enough. This is typical of all problems considered infeasable in computational complexity theory. The doubling of computational power that is happening due to Moores law still isn't good enough to solve many problems

$\endgroup$
1
  • $\begingroup$ How do you define "many"? Google for "SAT solver applications" to find many examples of large-scale real-world problems that are routinely being solved. Thanks for providing an example of the misleading statements that are often made in connection with computational complexity that the moral in my answer speaks against. $\endgroup$
    – Rob Arthan
    Dec 22, 2020 at 22:06

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .