MD5, SHA-1, and SHA-256 are fundamental cryptographic hash functions that produce a hash of fixed size given a message of arbitrary finite size. Their core components are compression functions. The MD5 compression function operates in 4 rounds of 16 steps each, while that of SHA-1 and SHA-256 operate in 80 and 64 rounds, respectively. It is computationally infeasible to invert these compression functions, i.e., to find an input given an output. In 2012, 28-step MD5, 23-round SHA-1, and 16-round SHA-256 compression functions were reduced to SAT and inverted by Conflict-Driven Clause Learning solvers, yet no progress in this area has been made since then. The present paper proposes to construct intermediate inverse problems for any pair of MD5 steps (i,i+1) such that the first problem is very close to inverting i steps, while the last one is almost inverting i+1 steps. The same idea works for a pair of sequential rounds in case of SHA-1 and SHA-256. SAT encodings of intermediate problems for MD5, SHA-1, and SHA-256 were constructed, and then a Conflict-Driven Clause Learning solver was parameterized on the simplest of them. The parameterized solver was used to design a parallel Cube-and-Conquer solver that for the first time inverted 29-step MD5, 24-round SHA-1, and 19-round SHA-256 compression functions.

We enumerate all extended self-orthogonal diagonal Latin squares of order up to 10. Our method reduces the problem of enumerating extended self-orthogonal diagonal Latin squares to a satisfiability (SAT) problem, and we find all solutions of the SAT problem using a SAT solver. We additionally show that there is no triple of mutually orthogonal diagonal Latin squares of order 10 containing an extended self-orthogonal diagonal Latin square.

The article gives the problem of resource assignment and performance optimisation in intelligent supply chain (ISC). The task of the resource assignment for intelligent supply chain is multi-product and multi-criterion task. Scale of the ISC determines the allocation of the suppliers and consumers of product. The customer demands for certain kind of product in ISC can be deemed as stochastic process. As goal of performance optimization task we should to evaluate parameters of ISC through assignment of production resources. The article presents the resource assignment model of ISC and its performance measures. On the base of simulation the verification and validation of presented model is carried out. The problem statement, solution method, numerical example and validation of model via simulation are represented for resource assignment and performance optimization model. Copyright (C) 2024 The Authors. This is an open access article under the CC BY-NC-ND license (https://creativecommons.org/licenses/by-nc-nd/4.0/)

Volunteer computing is a cheap yet efficient type of distributed computing, where desktops of private persons are united into projects. Some of these projects are aimed at finding new mathematical objects based on orthogonal systems of Latin squares. In 2021, new systems of orthogonal diagonal Latin squares of order 10 were found in a volunteer computing project. This was done using cells mapping schemes related to extended self-orthogonal diagonal Latin squares. In the present study, a classification of such schemes is proposed. The classification is built upon a structure of a multiset of cycle lengths, when a scheme is considered a permutation. For orders 1–9, the classification is constructed completely on a computer, while for order 10 only some classes are determined via volunteer computing. Finally, for order 10 new orthogonal systems were investigated using the cells mapping schemes and a SAT solver on a computer. It is described how the latter results can lead to finding the remaining classes for order 10 via volunteer computing.

MD5 and SHA-1 are fundamental cryptographic hash functions proposed in 1990s. Given a message of arbitrary finite size, MD5 produces a 128-bit hash in 64 steps, while SHA-1 produces a 160-bit hash in 80 steps. It is computationally infeasible to invert MD5 and SHA-1, i.e. to find a message given a hash. In 2012, 28-step MD5 and 23-step SHA-1 were inverted by CDCL solvers, yet no progress has been made since then. The present paper proposes to construct 31 intermediate inverse problems for any pair of MD5 or SHA-1 steps ( i, i + 1), such that the first problem is very close to inverting i steps, while the 31st one is almost inverting i + 1 steps. We constructed SAT encodings of intermediate problems for MD5 and SHA-1, and tuned a CDCL solver on the simplest of them. Then the tuned solver was used to design a parallel Cube-and-Conquer solver which for the first time inverted 29-step MD5 and 24-step SHA-1.

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.

MD4 and MD5 are fundamental cryptographic hash functions proposed in the early 1990s. MD4 consists of 48 steps and produces a 128-bit hash given a message of arbitrary finite size. MD5 is a more secure 64-step extension of MD4. Both MD4 and MD5 are vulnerable to practical collision attacks, yet it is still not realistic to invert them, i.e., to find a message given a hash. In 2007, the 39-step version of MD4 was inverted by reducing to SAT and applying a CDCL solver along with the so-called Dobbertin's constraints. As for MD5, in 2012 its 28-step version was inverted via a CDCL solver for one specified hash without adding any extra constraints. In this study, Cube-and-Conquer (a combination of CDCL and lookahead) is applied to invert step-reduced versions of MD4 and MD5. For this purpose, two algorithms are proposed. The first one generates inverse problems for MD4 by gradually modifying the Dobbertin's constraints. The second algorithm tries the cubing phase of Cube-and-Conquer with different cutoff thresholds to find the one with the minimum runtime estimate of the conquer phase. This algorithm operates in two modes: (i) estimating the hardness of a given propositional Boolean formula; (ii) incomplete SAT solving of a given satisfiable propositional Boolean formula. While the first algorithm is focused on inverting step-reduced MD4, the second one is not area-specific and is therefore applicable to a variety of classes of hard SAT instances. In this study, 40-, 41-, 42-, and 43-step MD4 are inverted for the first time via the first algorithm and the estimating mode of the second algorithm. Also, 28-step MD5 is inverted for four hashes via the incomplete SAT solving mode of the second algorithm. For three hashes out of them, it is done for the first time.

This study focuses on searching for pairs of orthogonal diagonal Latin squares of order 10. Consider a cells mapping in accordance to which one diagonal Latin square is mapped to another one. Given a certain cells mapping schema, the problem is to find a pair of orthogonal diagonal Latin squares of order 10 such that they match the schema (or to prove that such a pair does not exist). The problem is reduced to the Boolean satisfiability problem (SAT). Three mapping schemes are considered, and for each of them a SAT instance is constructed. If a satisfying assignment is found for an instance, the corresponding pair of orthogonal Latin squares can be easily extracted from it. The Cube-and-Conquer approach is used to solve the instances. The cubing phase is performed on a sequential look-ahead SAT solver, while on the conquer phase an experiment in a BOINC-based volunteer computing project is launched. In the experiment, for two out of three schemes orthogonal pairs are found.

The paper presents the approach to competences in the context of the problem of the distance learning process. The place of the problem of determining competence in ODL is analyzed. Competence in ODL conditions is becoming one of the basic instruments for assessing the quality of the learning process. Therefore, it is important to develop the theoretical basis for modeling competences and adapt this model to practical needs. An approach combining methods of game theory and fuzzy sets would allow determining the degree of competence possessed and acquired by all participants in the teaching process. In the paper the new educational model developed on acquiring the project team competence is represented. The issue of selecting partners to work on the project profile is being considered. The quality of the project team is determined by the degree of coverage of the domain of the project profile by the competences of its participants..

The paper describes advantages of teaching and application of modelling manufacturing systems. Two paradigms of modelling: Queuing systems and Simulation are briefly presented and analysed. Advantages of distance learning these approaches worldwide are presented. Furthermore, a combined way of learning these two methods, with a focus on the modelling and simulating selected basic processes of manufacturing systems, is proposed in briefly described case study. The concept provides division of this method depending on student's education level.

A description of a program for computation of acoustic fields in 3D shallow-water waveguides of arbitrary form is presented. This program is a C++ implementation of a numerical solver of wide-angle mode parabolic equations. The user can specify sound speed distribution, bottom relief, and the structure of bottom layers via configuration files when performing acoustic field simulation. The output of the program consists of one or several horizontal cut planes of the acoustic pressure field at specified depths. One of the main advantages of the implemented method is its high computational efficiency. The developed program is open-source and available online. It can be of interest for specialists in different areas of ocean acoustics who perform the modeling of sound propagation in course of the solution of various practical problems.

We consider a fundamental problem in the theory of branching heuristics for tree-based solvers, applicable e.g. to SAT, #SAT, CSP, #CSP. Such tree-based solvers are used as the cubing-part in the Cube-and-Conquer paradigm, and are thus of renewed interest for general (#)SAT solving. These solvers build at least implicitly a branching (backtracking) tree, with the goal to minimise tree-size. The heuristics are based on evaluating the progress made in a transition from an instance F to some “simplified” F' by a distance d(F,F') (the bigger the more progress). When a branching (F'_1, … , F'_k) is to be chosen for F, for each possibility we consider its branching tuple t given by t_i = d(F, F'_i) , project it to a single number π (t) , and choose a branching with minimal π (t) . This paper investigates the choices for π (t) , in a theoretical framework. The general theory is reviewed, together with the theoretical result on the “canonical projection” π (t) = τ (t) . Focusing then on binary branchings ( k=2 , t = (a,b) ), we analyse the asymptotics of τ (a,b) , and reflect on the whole possible range of binary projections, arriving at first practical possibilities for dynamic heuristics.

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.

We propose an algorithm for enumerating diagonal Latin squares. It relies on specific properties of diagonal Latin squares to employ symmetry breaking techniques. Furthermore, the algorithm employs several heuristic optimizations and bit arithmetic techniques. We use the algorithm to enumerate diagonal Latin squares of order at most 9.

We study an adaptive network model driven by a nonlinear voter dynamics. Each node in the network represents a voter and can be in one of two states that correspond to different opinions shared by the voters. A voter disagreeing with its neighbor's opinion may either adopt it or rewire its link to another randomly chosen voter with any opinion. The system is studied by means of the pair approximation in which a distinction between the average degrees of nodes in different states is made. This approach allows us to identify two dynamically active phases: a symmetric and an asymmetric one. The asymmetric active phase, in contrast to the symmetric one, is characterized by different numbers of nodes in the opposite states that coexist in the network. The pair approximation predicts the possibility of spontaneous symmetry breaking, which leads to a continuous phase transition between the symmetric and the asymmetric active phases. In this case, the absorbing transition occurs between the asymmetric active and the absorbing phases after the spontaneous symmetry breaking. Discontinuous phase transitions and hysteresis loops between both active phases are also possible. Interestingly, the asymmetric active phase is not displayed by the model where the rewiring occurs only to voters sharing the same opinion, studied by other authors. Our results are backed up by Monte Carlo simulations.