4 ms·
Of course, dividing search space into K pieces is not guaranteed to give you a speed-up _in the worst case_: you might pick an unlucky division where K-1 pieces
by madars 2y ago
Of course, dividing search space into K pieces is not guaranteed to give you a speed-up _in the worst case_: you might pick an unlucky division where K-1 pieces are easily UNSAT but the last remaining piece is as hard as the original (so the wall clock time is unchanged). However, in practice variable-fixing can and often does give an _expected time_ speed-up, especially if the SAT instance has some inherent parallel search structure (e.g., key or midstate bits for ciphers) and such heuristic tactics are still useful.
- almostgotcaught 2y ago> However, in practice variable-fixing can and often does give an _expected time_ speed-up Proof? Because as far as I know literally none of RP, BPP, ZPP relationships to NP are known.
- madars 2y agoIndeed no proof. By "in practice" I meant "on instances encountered in real-world applications."
- almostgotcaught 2y agothen instead of _expected time_ you should say _hope-for time_ because _expected time_, in this context, is already firmly defined.
- deleted 2y ago[deleted]