In recent years, constraint solvers show increasing use in solving various open combinatorial problems, e.g., from Ramsey theory or synthesis of combinatorial designs. The similar approach can be applied to some problems related to binary linear codes, which form one of the largest families of error correcting codes used both in coding theory and in various practical applications. Thanks to a simple algebraic structure of such codes it is possible to study them using a wide range of methods. Note that even codes with the same basic parameters (length n, dimension k, minimum code distance d) can show different error correction performance, i.e., the ability to correct errors which appear in a noisy channel. In the paper, we formulate the problem of finding binary linear codes with good error correction performance as a constraint optimization problem and explore the effectiveness of modern constraint solvers on it, including SAT, MaxSAT, and CP solvers. Using the respective solvers and parallel computing, for several values of n, k, d we found the codes which are significantly better than the known in terms of their practical performance.

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.

Backdoors for SAT, proposed by Williams et al. in 2003, are the sets of variables, the instantiation of which vastly simplifies the resulting subproblem. The focus of the present paper are ρ-backdoors — the probabilistic generalization of Strong Backdoor Sets. Unlike most kinds of backdoors, small ρ-backdoors with ρ > 0 are relatively easy to find and they can be found in many formulas. In the theoretical part of the paper, we show that there exists a connection between ρ-backdoors and the conflict information generated by CDCL SAT solvers. On the one hand, any set of variables appearing in some learnt clauses can be viewed as a ρ-backdoor (with ρ > 0) with respect to the Unit Propagation (UP) rule. On the other hand, surprisingly, ρ-backdoors can often be used to generate logical entailments of a formula, which can be viewed as learnt clauses, and we present several techniques and algorithms, that can be used to derive such clauses. We also show that a ρ-backdoor with ρ > 0 can be considered as a partial unsatisfiability certificate for a CNF formula as it proves that the formula is false for the fraction of at least ρ of all possible assignments. Therefore, from the practical viewpoint, finding ρ-backdoors with ρ close to 1 makes sense. To evaluate the proposed techniques, we implemented a proof-of-concept prototype, that interleaves the backdoor-based techniques with standard CDCL solving, and evaluated it on a variety of challenging benchmarks. The results of the experiments show that the proposed technique makes it possible to speed up the SAT solving for many hard SAT instances both from SAT Competitions and of industrial origin.

The concept of Strong Backdoor Sets (SBS) for Constraint Satisfaction Problems is well known as one of the attempts to exploit structural peculiarities in hard instances. However, in practice, finding an SBS for a particular instance is often harder than solving it. Recently, a probabilistic weakened variant of the SBS was introduced: in the SBS, all subproblems must be polynomially solvable, whereas in the probabilistic SBS only a large fraction ρ of them should have this property. This new variant of backdoors called ρ-backdoors makes it possible to use the Monte Carlo method and metaheuristic optimization to find ρ-backdoors with ρ very close to 1, and relatively fast. Despite the fact that in a ρ-backdoor-based decomposition a portion of hard subproblems remain, in practice the narrowing of the search space often allows solving the problem faster with such a backdoor than without it. In this paper, we significantly improve on the concept of ρ-backdoors by extending this concept to backdoor trees: we introduce ρ-backdoor trees, show the interconnections between SBS, ρ-backdoors, and the corresponding backdoor trees, and establish some new theoretical properties of backdoor trees. In the experimental part of the paper, we show that moving from the metaheuristic search for ρ-backdoors to that of ρ-backdoor trees allows drastically reducing the time required to construct the required decompositions without compromising their quality.

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.

In the present paper, we propose a technology for translating algorithmic descriptions of discrete functions to SAT. The proposed technology is aimed at applications in algebraic cryptanalysis. We describe how cryptanalysis problems are reduced to SAT in such a way that it should be perceived as natural by the cryptographic community. In~the theoretical part of the paper we justify the main principles of general reduction to SAT for discrete functions from a class containing the majority of functions employed in cryptography. Then, we describe the Transalg software tool developed based on these principles with SAT-based cryptanalysis specifics in mind. We demonstrate the results of applications of Transalg to construction of a number of attacks on various cryptographic functions. Some of the corresponding attacks are state of the art. We compare the functional capabilities of the proposed tool with that of other domain-specific software tools which can be used to reduce cryptanalysis problems to SAT, and also with the CBMC system widely employed in symbolic verification. The paper also presents vast experimental data, obtained using the SAT solvers that took first places at the SAT competitions in the recent several years.

Propositional satisfiability (SAT) is at the nucleus of state-of-the-art approaches to a variety of computationally hard problems, one of which is cryptanalysis. Moreover, a number of practical applications of SAT can only be tackled efficiently by identifying and exploiting a subset of formula's variables called backdoor set (or simply backdoors). This paper proposes a new class of backdoor sets for SAT used in the context of cryptographic attacks, namely guess-and-determine attacks. The idea is to identify the best set of backdoor variables subject to a statistically estimated hardness of the guess-and-determine attack using a SAT solver. Experimental results on weakened variants of the renowned encryption algorithms exhibit advantage of the proposed approach compared to the state of the art in terms of the estimated hardness of the resulting guess-and-determine attacks.

In this paper we propose the technology for constructing propositional encodings of discrete functions. It is aimed at solving inversion problems of considered functions using state-of-the-art SAT solvers. We implemented this technology in the form of the software system called TRANSALG, and used it to construct SAT encodings for a number of cryptanalysis problems. By applying SAT solvers to these encodings we managed to invert several cryptographic functions. In particular, we used the SAT encodings produced by TRANSALG to construct the family of two-block MD5 collisions in which the first 10 bytes are zeros. In addition to that we used TRANSALG encoding for the widely known A5/1 keystream generator to solve several dozen of its cryptanalysis instances in a distributed computing environment. Also in the present paper we compare the functionality of TRANSALG with that of similar software systems.

The Earth's atmosphere heavily affects the remote sensing images collected by spaceborne passive optical sensors due to radiation–matter interaction phenomena like radiation absorption, scattering, and thermal emission. A complex phenomenon is the adjacency effect, i.e., radiation reflected by the ground that, due to the atmospheric scattering, is being seen in a viewing direction different from that corresponding to the ground location that reflected it. Adjacency gives rise to crosstalk between neighboring picture elements up to a distance that depends on the width of the integral kernel function employed for the mathematical modeling of the problem. As long as the atmosphere is a linear space-invariant system, the adjacency can be modeled as a low-pass filter, with the atmospheric point spread function (APSF) applied to the initial image. In this paper, a direct method of estimating the discrete normalized APSF (NAPSF) using images gathered by high-resolution optical sensors is discussed. We discuss the use of the NAPSF estimate for deducing the Correction Spatial high-pass Filter (CSF)—a correction filter that removes the adjacency effect. The NAPSF estimation procedure has been investigated using statistical simulations, whose outcomes permitted us to identify the conditions under which the NAPSF could be measured with acceptable errors. The NAPSF estimation is examined for various natural images acquired by MOMS-2P, CHRIS, AVIRIS, and MIVIS.