SAT solvers can solve logical problems much faster than brute force. They take advantage of heuristics, and they use certain mathematical techniques to rule out

SAT solvers can solve logical problems much faster than brute force. They take advantage of heuristics, and they use certain mathematical techniques to rule out parts of the search space and narrow it down significantly. In general most crypto can't be broken by solvers. The solvers might be faster than brute force, but still take exponential amounts of time to solve it. However if the crypto was designed badly, there can be weaknesses in it that the solvers can find and exploit. It's basically like those logic puzzles that are sometimes asked to kids. I don't have a specific example handy, but they go like "Fred won't sit next to Bill. Bill wants to sit next to Mary. Mary wants to sit in the same table as Ned..." And then they ask you to find a seating arrangement that satisfies all these constraints. You can try every possibility, and there are exponentially many as you add more people. But if you are clever, you can realize certain constraints rule out large portions of the search space. Like you know the answer must have Mary in the same table as Ned, so you don't even try any possibilities where that's not true. There are many other clever tricks SAT solvers use to shrink the search space.