Can anyone help with what looks like SAT scalability problem? Is there a modern SAT solver that can do it? I was trying out Google SAT and it seems not to be able to scale to a simple school scheduling problem. Here’s the post with the code and test data https://groups.google.com/forum/m/#!topic/or-tools-discuss/O...
In the worst case we can't get around exponential runtime in the problem size. This is problematic since encoding often is not even linear but quadratic or worse. But there are often tricks to get to encoding to nlogn size.
Problems that are "hard" are usually specially crafted (SAT competition).
Getting back to your question: In practice most problems do not show exponential runtime behaviour. Using a good SAT solver is key here since the more naive an implementation is, the more probable it is to run into exponential runtime with practical problems.
