Аннотация:
The Boolean satisfiability problem (SAT) is a classical combinatorial problem which is NP-complete in the decision variant and NP-hard in the search variant. Nevertheless, during the recent 20 years there have been developed a lot of applied algorithms that successfully tackle SAT for formulas of large dimension
(tens of thousands of variables and hundreds of thousands of clauses). These algorithms called SAT solvers are routinely used in such areas as symbolic verification, program testing, cryptanalysis, bioinformatics, combinatorics, etc. Despite the impressive effectiveness of modern SAT solvers, it is often important to know in advance their approximate runtime on particular formulas. It is a typical situation that a SAT solver has been working for an hour or a day or a month, and it is not known whether it will finish anytime soon. The question then is whether it is possible to construct some meaningful upper bounds on the runtime of a particular SAT solver on a particular SAT instance? In the report we will present several results in this direction. The presented approach is based on the idea to evaluate the hardness of a formula via some decomposition or, in a more general case, via a so-called SAT partitioning of a formula. In order to construct such a partitioning we choose a set called Backdoor and decompose an original formula into sub-formulas by substituting all possible combinations of values of backdoor variables to a formula. Then, under certain assumptions we can use the Monte Carlo method to estimate the runtime of a solver on the original formula via its runtimes on formulas from a constructed decomposition. On the level of ideas, the proposed estimations are quite close to the hardness estimations that are constructed based on the knowledge of the so-called Strong Backdoor Sets. In the report we will show the interconnection between Strong Backdoors and the proposed notions, and present the results of computational experiments which demonstrate the practical applicability using backdoors to estimate the hardness of Boolean formulas. We will also briefly describe the basic algorithms and techniques used in state-of-the-art SAT solvers.
