Author name cluster

Stepan Kochemazov

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

AAAI Conference 2026 Conference Paper

Using Constraint Solvers to Construct Binary Codes with Good Error Correction Performance

Stepan Kochemazov
Oleg Zaikin
Grigorii Trofimiuk
Kirill Antonov
Alexander Semenov

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.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Using Backdoors to Generate Learnt Information in SAT Solving

Alexander Andreev
Konstantin Chukharev
Stepan Kochemazov
Alexander A. Semenov

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.

Details

AAAI Conference 2023 Conference Paper

Probabilistic Generalization of Backdoor Trees with Application to SAT

Alexander Semenov
Daniil Chivilikhin
Stepan Kochemazov
Ibragim Dzhiblavi

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.

PDF Details DOI

AAAI Conference 2022 Conference Paper

On Probabilistic Generalization of Backdoors in Boolean Satisfiability

Alexander Semenov
Artem Pavlenko
Daniil Chivilikhin
Stepan Kochemazov

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.

PDF Details

SAT Conference 2021 Conference Paper

Assessing Progress in SAT Solvers Through the Lens of Incremental SAT

Stepan Kochemazov
Alexey Ignatiev
João Marques-Silva 0001

Abstract 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.

Details

SAT Conference 2020 Conference Paper

Improving Implementation of SAT Competitions 2017-2019 Winners

Stepan Kochemazov

Abstract The results of annual SAT competitions are often viewed as the milestones showcasing the progress in SAT solvers. However, their competitive nature leads to the situation when the majority of this year’s solvers are based on previous year’s winner. And since the main focus is always on novelty, it means that there are times when some implementation details have a potential for improvement, but they are just inherited from solver to solver for several years in a row. In this study we propose small modifications of implementations of existing heuristics in several related SAT solvers. These modifications mostly consist in employing a deterministic strategy for switching between branching heuristics and in augmentations of the treatment of Tier2 and Core clauses. In our experiments we show that the proposed changes have a positive effect on solvers’ performance both individually and in combination with each other.

Details

ECAI Conference 2020 Conference Paper

Speeding Up CDCL Inference with Duplicate Learnt Clauses

Stepan Kochemazov
Oleg Zaikin 0002
Alexander A. Semenov
Victor Kondratiev

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 relearned 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.

Details

SAT Conference 2018 Conference Paper

ALIAS: A Modular Tool for Finding Backdoors for SAT

Stepan Kochemazov
Oleg Zaikin 0002

Abstract We present ALIAS, a modular tool aimed at finding backdoors for hard SAT instances. Here by a backdoor for a specific SAT solver and SAT formula we mean a set of its variables, all possible instantiations of which lead to construction of a family of subformulas with the total solving time less than that for an original formula. For a particular backdoor, the tool uses the Monte-Carlo algorithm to estimate the runtime of a solver when partitioning an original problem via said backdoor. Thus, the problem of finding a backdoor is viewed as a black-box optimization problem. The tool’s modular structure allows to employ state-of-the-art SAT solvers and black-box optimization heuristics. In practice, for a number of hard SAT instances, the tool made it possible to solve them much faster than using state-of-the-art multithreaded SAT-solvers.

Details

AAAI Conference 2018 Conference Paper

On Cryptographic Attacks Using Backdoors for SAT

Alexander Semenov
Oleg Zaikin
Ilya Otpuschennikov
Stepan Kochemazov
Alexey Ignatiev

Propositional satisﬁability (SAT) is at the nucleus of state-ofthe-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 efﬁciently 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-anddetermine 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.

PDF Details

ECAI Conference 2016 Conference Paper

Encoding Cryptographic Functions to SAT Using TRANSALG System

Ilya V. Otpuschennikov
Alexander A. Semenov
Irina Gribanova
Oleg Zaikin 0002
Stepan Kochemazov

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.

Details