3 ms·
Yes, NP-hardness is a worst-case notion, hence not easy to use in cryptography. But, once you know what algorithms and heuristics the SAT solver is using, it's
by mafribe 13y ago
Yes, NP-hardness is a worst-case notion, hence not easy to use in cryptography.
But, once you know what algorithms and heuristics the SAT solver is using, it's usually not hard to concoct propositional formulae that the prover chokes on. It just happens to be the case that the formulae that humans typically want to get solved are easy for the algorithms we use. Quite why this is nobody really knows.
Also, the reason we typically reduce NP hard-problems to SAT is not that SAT is somehow easier than other NP-hard problems, but because so much effort has been spent on optimising SAT solvers, unlike for almost all other NP-hard problems. As you say, when you reduce a problem to SAT, you typically loose a lot of structure. But the decades of research on SAT solvers more than compensate.
- mjn 13y agoI think it's mostly true that SAT-solvers are better because of decades of research/engineering on them. However there is some speculation that your observation that "you typically lose a lot of structure" is actually sometimes a win, because by "flattening" a representation it might allow some distant implicit constraints to propagate. In planning, for example, that's one hypothesis for where Graphplan and SATplan (two 1990s systems) got their win from, vs. traditional symbolic planners. Similar to a question that comes up in compilers, about optimizing high-level vs. low-level representations. High-level representations give you more specific semantic information, but turning everything into a flattened mud of combinator logic or CPS or SSA might allow for some whole-program optimizations that propagate originally-distant constraints.