4 ms·
This SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size. It's all about the diffic
by nightcracker 6y ago
This SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size.
It's all about the difficulty vs the size of the instance.
- jlokier 6y agoTo the best of my knowledge, the example has no known heuristics for finding a solution that are significantly faster than brute force. That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.
- nightcracker 6y agoA SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give. The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion. So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.