In this paper we propose new evolutionary algorithms for finding the so-called backdoors - special structures that make it possible to simplify the solving of combinatorial problems expressed as systems of constraints. In particular, we consider the Boolean satisfiability problem (SAT) and search for ρ-backdoors for Boolean formulas. We analyze the problem of finding ρ-backdoors of small fixed size and adapt (1+1)-EA for its solving: in the proposed algorithm the mutation is performed in such a way that it transitions between Boolean vectors of fixed weight. The proposed algorithm was implemented in the context of a parallel asynchronous strategy based on the island paradigm. In the experimental part we demonstrate the applicability of this algorithm by using the found backdoors to solve extremely hard instances from the area of Logical Equivalence Checking for Boolean circuits: our approach on this class of benchmarks outperforms the best state-of-the-art SAT solvers.

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables B a ρ-backdoor, if for a fraction of at least ρ of possible assignments of variables from B, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a ρ-backdoor with ρ=1 is an SBS. For a given set B it is possible to efficiently construct an (ε, δ)-approximation of parameter ρ using the Monte Carlo method. Thus, we define an (ε, δ)-SBS as such a set B for which the conclusion "parameter ρ deviates from 1 by no more than ε" is true with probability no smaller than 1 - δ. We consider the problems of finding the minimum SBS and the minimum (ε, δ)-SBS. To solve the former problem, one can use the algorithm described by R. Williams, C. Gomes and B. Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter problem, and show that the asymptotic estimation of the worst-case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams et al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal (ε, δ)-SBS. Results of computational experiments show that the use of (ε, δ)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.

In this work we propose an asynchronous parallel evolutionary algorithm that is efficient for a specific type of gray-box optimization problems, in which the calculation of the fitness function may be split into a set of several independent calculations. An example of such an optimization problem is the search for backdoors (hidden structures) in the Boolean satisfiability problem: subsets of variables that allow an efficient splitting of the problem into a set of independent subproblems. Our experiments show that the proposed asynchronous approach allows speeding up the algorithm considerably, while also effi-ciently utilizing comnuting cluster time.

Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε,δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

Algebraic cryptanalysis studies breaking ciphers by solving algebraic equations. Some of the promising approaches use SAT solvers for this purpose. Although the corresponding satisfiability problems are hard, their difficulty can often be lowered by choosing a set of variables to brute force over, and by solving each of the corresponding reduced problems using a SAT solver, which is called the guess-and-determine attack. In many successful cipher breaking attempts this set was chosen analytically, however, the nature of the problem makes evolutionary computation a good choice.