4 ms·
> SAT is pretty much a solved problem We don’t really understand what makes some SAT problems harder than others. You can go from a problem solvable with CDCL
by fooker 3y ago
> SAT is pretty much a solved problem
We don’t really understand what makes some SAT problems harder than others.
You can go from a problem solvable with CDCL in a few seconds to one that would outlast the solar system by changing a couple of input bits.
- ngruhn 3y agoSure, but in practice that’s not what people worry about, from what I have seen. At least when dealing with SMT problems, the SAT part is the easy part.
- empath-nirvana 3y agoI think that's because _in practice_ people don't waste their time working on intractable problems if they just want to get something done. There's almost always some way to avoid the intractable problem and approach it a different way. It's sort of like how "in practice" it didn't matter for thousands of years that nobody understood electricity. Any problem that came up that would have required that knowledge to solve just got dropped, because they didn't have the tools to solve it.