We study a class of location problems formulated for a bipartite graph: the vertices from one part of the graph interpret clients while the vertices from the second part correspond to facilities that serve the clients. The goal is to close as many facilities as possible so that the number of dissatisfied clients does not exceed the pre-specified threshold. This formulation corresponds to the so-called Branch Location Problem (BLP). In the paper we reduce BLP to Integer Linear Programming (ILP) and Maximum Satisfiability (MaxSAT). To solve the instances of these combinatorial problems we employ complete 0-1-ILP and MaxSAT solvers, as well as one metaheuristic (MVP) which can be viewed as a variant of the well known Variable Neighborhood Search (VNS) algorithm. We construct families of random BLP instances of varying dimensions and demonstrate in the computational experiments that the MVP-based algorithms show good performance on such instances: in most cases they find the global optimum and spend significantly less time on solving compared to complete solvers.

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 the paper we consider the well-known Influence Maximization (IM) and Target Set Selection (TSS) problems for Boolean networks under Deterministic Linear Threshold Model (DLTM). The main novelty of our paper is that we state these problems in the context of pseudo-Boolean optimization and solve them using evolutionary algorithms in combination with the known greedy heuristic. We also propose a new variant of (1 + 1)-Evolutionary Algorithm, which is designed to optimize a fitness function on the subset of the Boolean hypercube comprised of vectors of a fixed Hamming weight. The properties of this algorithm suit well for solving IM. The proposed algorithm is combined with the greedy heuristic for solving IM and TSS: the latter is used to construct initial solutions. We show that the described hybrid algorithms demonstrate significantly better performance compared to the computational scheme combining the greedy heuristic with the classic variant of (1 + 1)-EA. In the experiments, the proposed algorithms are applied to both real-world networks and the random networks constructed with respect to well-known models of random graphs. The results show that the new algorithms outperform the competition and are applicable to TSS and IM under DLTM for networks with tens of thousands of vertices.

Many industrial verification problems are solved via reduction to CircuitSAT (curcuit satisfibiliaty). It is often the case that the resulting SAT instances are very hard and require the use of parallel computing to be solved in reasonable time. The particularly relevant problem in this context is how to best plan the use of the computing resources, because SAT solvers' runtime is well known to be hard to predict. In the present paper we propose two methods that employ the knowledge about a circuit's structure to partition a CircuitSAT instance into a specific number of simpler subproblems. A distinctive feature of the proposed partitioning methods is that they make it possible to estimate the hardness (e.g. the total runtime of a SAT solver on all subproblems) of a partitioning via the Monte Carlo method. In the experimental evaluation we apply these methods to hard CircuitSAT instances and compare their performance with the well known Cube and Conquer approach. The proposed partitioning methods not only often outperform Cube and Conquer, but also show remarkably small variance in the runtime of a SAT solver on subproblems from a partitioning, thus making it possible to construct accurate estimations of time required to process all subproblems, using random samples of small size. As a consequence, we have the efficient stochastic estimation procedure which provides an additional opportunity to employ hyperparameter tuning methods to further increase the SAT solver performance on (partitioned) hard SAT instances. We demonstrate the effectiveness of the proposed constructions by applying them to some problems associated with CircuitSAT, in particular, Logical Equivalence Checking benchmarks, Automated Test Pattern Generation benchmarks and the inversion problems of some cryptographic functions.

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 rho-backdoors with rho > 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 rho-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 rho> 0) with respect to the Unit Propagation (UP) rule. On the other hand, surprisingly, rho-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 rho-backdoor with rho > 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 rho of all possible assignments. Therefore, from the practical viewpoint, finding rho-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.

In the paper we consider the discrete variant of the well-known Influence Maximization Problem (IMP). Given some influence model, it consists in finding a so-called seed set of influential users of fixed size, that maximizes the total spread of influence over the network. We limit our study to the influence model called Deterministic Linear Threshold Model (DLTM). It is well known that IMP under DLTM is computationally hard and there are no approximate algorithms for its solving with a constant approximation ratio if $P\neq NP$. Therefore, it makes sense to apply metaheuristic algorithms to this problem. In the present research we propose new algorithms for solving IMP under DLTM, which are based on a technique that combines evolutionary and genetic strategies for pseudo-Boolean optimization with a greedy algorithm which is used to find some initial approximation. We use the proposed strategy to solve another well-known combinatorial problem for networks called Target Set Selection (TSS). We propose to solve TSS as a sequence of IMPs with gradually decreasing of target set size. In the experimental part of the paper we demonstrate that our new strategy outperforms the previous ways to solve TSS, yielding smaller target sets of good quality.

Inversion of reduced-round hash functions is one of the areas of cryptography, in which Boolean satisfiability (SAT) solvers show good performance. Recent results on the inversion of 43 -step MD4 using SAT make it possible to believe that more progress can be achieved by careful solver engineering and SAT encodings manipulation. In the present paper we consider possible ways to improve the SAT encodings for inversion of hash functions from the MD and SHA families, in particular, MD4, and SHA-1. We study the available encodings, including the ones proposed by Vegard Nossum, and made by automatic encoding tools. We then show that it is possible to make the encodings better by constructing the integer sums in a different way or eliminating some of the auxiliary variables via Boolean minimization. In the computational experiments we consider a variety of benchmarks, which encode reduced-round variants of the considered hash functions.

In this paper we describe a class of cryptographic guess-and-determine attacks which is based on the notion of a linearizing set. A linearizing set-based attack is applied to a system of Multivariate Quadratic equations (MQ) over $GF(2)$ field, which encodes how a considered cryptographic function works. By substituting into such MQ system a random (in some strict sense) assignment of variables from a linearizing set we aim to transform the system into a linear one. We introduce a probability of such an event and call it a probability of linearization. Then we describe a guess-and-determine attack, the hardness of which can be expressed via a probability of linearization. To estimate the latter it is possible to use a simple Monte Carlo algorithm. Also we describe a technique that allows to augment a considered MQ system by new linear equations and to construct a new MQ system, for which the probability of linearization is usually larger than that for an original one. For this purpose we apply a SAT oracle to a Boolean formula that is naturally associated with a considered MQ system. Finally, we reduce the problem of searching for a linearizing set that yields the best effectiveness of a constructed guess-and-determine attack to a pseudo-Boolean optimization problem, which can be solved using metaheuristic optimization algorithms. The important consequence of this is that this way we can construct guess-and-determine attacks automatically by solving the corresponding optimization problem. In the computational experiments we used the proposed methodology to construct attacks on several well-known stream ciphers. The runtime estimations of some of the attacks make it possible to implement them in reasonable time.

The Boolean satisfiability problem (SAT) and maximum satisfiability problem (MaxSAT) are among the most well-known combinatorial problems in today’s computer science. The algorithms for their solving also go hand-in-hand, in that most MaxSAT solvers employ SAT solvers as the so-called oracles. In the present paper we perform a computational study of the RC2 algorithm, which is among the best state-of-the-art algorithms for MaxSAT solving. We view it from the SAT oracle viewpoint and consider how the SAT oracle’s runtime is distributed among RC2 procedures and heuristics, and how this statistics differs depending on the SAT solver employed as an oracle. In addition to that we consider the two baseline MSE’18 configurations of RC2, analyze their performance and experiment with blending them together.

We propose a family of parallel algorithms aimed at solving problems related to hardware verification. We consider the Logical Equivalence Checking problem (LEC) and a particular case known as Automated Test Pattern Generation (ATPG). The main algorithmic basis for solving LEC and ATPG consists of state-of-the-art SAT-solving algorithms. However, for extremely hard SAT instances, the situation often arises when we can say nothing about the runtime of the SAT solver on a considered instance. We can, nonetheless, estimate the runtime if we decompose the original instance into a family of simpler instances that can be solved in a reasonable time. As an additional bonus, this approach provides a means for solving a given problem in parallel. We exploit the described idea in some extremely hard ATPG instances in SAT form and demonstrate that parallel computing is essential for efficient ATPG solving.

In this paper we study the Target Set Selection problem (TSS) – the well-known combinatorial problem associated with collective behaviour in networks. For a given network graph and the information diffusion model that specifies a dynamic process of how vertices activate each other, TSS aims to identify a set of initially active vertices of minimum cardinality such that they manage to activate all the other network vertices. This problem is computationally hard but has numerous applications in practice, thus the development of computational algorithms for TSS is a relevant topic. A surprising fact is that the spectrum of algorithms for TSS presented so far in the literature is quite limited. The main novelty of our study consists in the hybrid approach which combines evolutionary and greedy algorithms for TSS. In more detail, we view TSS as a pseudo-Boolean optimization problem and solve it using simple evolutionary algorithms (in fact several variants of (1+1)-EA). In order to identify a good initial approximate solution we employ a greedy algorithm. In the experiments we apply the developed algorithms to TSS in the context of Deterministic Linear Threshold Model (DLTM) and demonstrate that the presented approach shows good effectiveness when solving TSS on networks with dozens thousands of vertices on personal computer.

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.

There is a wide consensus, which is supported by the hard experimental evidence of the SAT competitions, that clear progress in SAT solver performance has been observed in recent years. However, in the vast majority of practical applications of SAT, one is expected to use SAT solvers as oracles deciding a possibly large number of propositional formulas. In practice, this is often achieved through the use of incremental SAT. Given this fundamental use of SAT solvers, this paper investigates whether recent improvements in solver performance have an observable positive impact on the overall problem-solving efficiency in settings where incremental SAT is mandatory or at least expected. Our results, obtained on a number of well-known practically significant applications, suggest that most improvements made to SAT solvers in recent years have no positive impact on the overall performance when solvers are used incrementally.

SAT-based cryptanalysis implies using algorithms for solving the Boolean Satisfiability (SAT) problem to perform cryptographic attacks. It is a flourishing research field. Tackling individual subproblems constructed in the course of the so-called guess-and-determine attacks is the most straightforward way SAT solvers are used in cryptography. If the expected runtime of an attack is of the order of millions of hours, then it makes sense to try to squeeze any extra bit of performance out of the main algorithm. In this paper, our goal is to figure out possible ways to do exactly that with SAT solvers, going beyond simple parameter tuning. In particular, we consider tasks related to cryptanalysis of several modern keystream generators, analyze and prepare several modifications of state-of-the-art SAT solvers to tackling them, tune their parameters, and evaluate the speedup.

Solving hard instances of the Boolean satisfiability problem (SAT) in practice is an interestingly nontrivial area. The heuristic nature of SAT solvers makes it impossible to know in advance how long it will take to solve any particular SAT instance. One way of coping with this disadvantage is the Divide-and-Conquer approach when an original SAT instance is decomposed into a set of simpler subproblems. However, the way it is decomposed plays a crucial role in the resulting effectiveness of solving. In the present study, we reduce the problem of choosing a proper decomposition to a stochastic pseudo-Boolean black-box optimization problem. Several optimization algorithms of different types were used to analyse a number of hard SAT-based optimization problems, related to SAT-based cryptanalysis of state-of-the-art stream ciphers. A meticulous computational study showed that some of the considered optimization algorithms perform much better than the others in the context of the problems from the considered class. It turned out that the obtained results also pose some cryptographic interest.

In the present chapter we study one method for partitioning hard instances of the Boolean satisfiability problem (SAT). It uses a subset of a set of variables of an original formula to partition it into a family of subproblems that are significantly easier to solve individually. While it is usually very hard to estimate the time required to solve a hard SAT instance without actually solving it, the partitionings of the presented kind make it possible to naturally construct such estimations via the well-known Monte Carlo method. We show that the problem of finding a SAT partitioning with minimal estimation of time required to solve all subproblems can be formulated as the problem of minimizing a special pseudo-Boolean black-box function. The experimental part of the paper clearly shows that in the context of the proposed approach relatively simple black-box optimization algorithms show good results in application to minimization of the functions of the described kind even when faced with hard SAT instances that encode problems of finding preimages of cryptographic functions.

Conflict-driven clause learning (CDCL) is well-known to be the predominant SAT solving approach. Its main idea consists in using conflict clauses to guide the effective traversal of the complete search space. Despite the undoubted usefulness of this powerful mechanism, a CDCL solver may end up computing (exponentially) many conflict clauses. To resolve this issue, a number of efficient heuristics exist aiming at aggressive conflict clause filtering, which leads to some of the clauses being removed. Thus, when processing a particular instance, a solver may learn and remove the same clause multiple times. One might see it as an indication that such re-learned clauses pose extra value. In the paper we show that extracting duplicate clauses and storing them indefinitely can be beneficial for the CDCL solver performance which is indicated by the fact that the family of solvers incorporating the corresponding heuristic won in the UNSAT and SAT+UNSAT tracks of the SAT Race 2019. We perform the detailed experimental evaluation of this heuristic on the instances from the SAT Competitions 2017 and 2018, and also SAT Race 2019 and show that it improves both PAR-2 and SCR scores.

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.

The Conflict-Driven Clause Learning algorithms for solving the Boolean satisfiability problem comprise the major part of the methods used to solve various instances of the problems that arise in industry and science. In recent years there have been proposed several major heuristics for these algorithms which are assumed to be de facto good for the solvers’ performance over diverse sets of benchmarks. The goal of this paper is to evaluate the contribution of each separate heuristic to the performance of a state-of-the-art solver, see the extent to which they are beneficial, and figure out if the heuristics have any particular features that need to be taken into account.