Lesson 1

The code above clearly demonstrates how convenient it is to use the language of the satisfiability problem and how effective SAT solvers are in practice. And all this despite the fact that we still do not know a single algorithm that is guaranteed to solve the satisfiability problem in time \((2-\varepsilon)^{n}\operatorname{poly}(|F|)\), where \(n\) is the number of variables of the input formula \(F\), and \(\varepsilon>0\) is a constant. At the same time, solving in time \(2^{n}\operatorname{poly}(|F|)\) is easy: this is just an exhaustive search of the entire search space (that is, all potential satisfying assignments). That is, SAT solvers find a satisfying assignment in a potentially huge search space clearly much faster than exhaustive search, but we cannot prove that they always do it quickly. This is the subject of a large number of studies. Recently, results have even begun to appear showing that speeding up some well-known algorithm is no easier than speeding up exhaustive search for the satisfiability problem. The area that studies such connections is called fine-grained complexity.