@skelk Another couple of points I would like to integrate in the discussion
On one hand, my experience is that the connection between hardness in practice and NP-hardness is tenuous at best. SAT solver are fail on well known easy formulas regularly, simply because solvers employ generic algorithms and do not have the time to try specialized approaches that could win only few cases (we should remember that state-of-the-art SAT solvers live or die by SAT competitions).
The notion of "it works in practice" may sometimes be a self-fulfilling prophecy. SAT solvers are not used to break crypto because they do not work well there, still that's a very practical application. They are used mostly in application where it turns out they are fast. Moreover, expert encoders avoid well-known hard structures. For example, they avoid structures like the ones in pigeonhole principle because that is very hard for Resolution.
=> More informations about this toot | View the thread | More toots from massimolauria@mathstodon.xyz
=> View skelk@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).