Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.



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


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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: