In this paper we consider the approach to solving the problem of search for systems of diagonal orthogonal Latin squares in the form of the Boolean Satisfiability problem. We describe two different propositional encod...
详细信息
In this paper we consider the approach to solving the problem of search for systems of diagonal orthogonal Latin squares in the form of the Boolean Satisfiability problem. We describe two different propositional encodings that we use. The first encoding is constructed for finding pairs of orthogonal diagonal Latin squares of order 10. Using this encoding we managed to find 17 previously unknown pairs of such squares using the volunteer computing project SAT@home. The second encoding is constructed for finding pseudotriples of orthogonal diagonal Latin squares of order 10. Using the pairs found with the help of SAT@home and the second encoding we successfully constructed several new pseudotriples of diagonal Latin squares of order 10.
In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encodin...
详细信息
In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encoding methods for formal computing models and on the concept of symbolic execution. We used the Transalg system to make SAT encodings for a number of cryptographic functions.
In this paper, a cryptanalysis of the Bivium keystream generator in the SAT form is considered. For encoding the initial cryptanalysis problem into SAT a special program system Transalg was used. For an obtained SAT i...
详细信息
In this paper, a cryptanalysis of the Bivium keystream generator in the SAT form is considered. For encoding the initial cryptanalysis problem into SAT a special program system Transalg was used. For an obtained SAT instance we use Monte Carlo method to search for a partitioning with good time estimation. Several weakened cryptanalysis instances of the Bivium generator were successfully solved in the volunteer computing project SAT@home using corresponding partitionings found on a computing cluster.
The paper presents a problem formulation for the development of a theoretical and software framework for creating systems of data extraction from arbitrary spreadsheet tables. The problem covers the tasks of the autom...
详细信息
This article focuses on development of software for calculating the temperatures and pressures of rock formation. The assessment of the physicochemical conditions of natural mineral formation is based on solving the i...
详细信息
The paper deals with the problem of optimal packing of two sets of circles (2-D spheres) into a simply connected container. The number of circles is given. The radii of these circles are equal within each set, but, ge...
详细信息
The paper deals with the problem of optimal packing of two sets of circles (2-D spheres) into a simply connected container. The number of circles is given. The radii of these circles are equal within each set, but, generally speaking, they differ between sets. There are two different statements of a such problem. The simplest one is when the circles of a larger radius are located first, and then smaller circles are packed into the gaps. Solving of a such problem, in fact, reduces to a two-fold solution of the equal circles packing problem. However, the procedure is complicated by the fact that in the second solution the container will be a multiply connected set. We consider a more complex formulation: it is required to maximize the radii of the circles when their ratio is fixed. The circle packing problem is usually studied in the case when the distance between points is Euclidean and even then belongs to the class of NP-hard problems. We assume that the distance is determined by means of some special metric, which, generally speaking, is not Euclidean. The special numerical algorithm is suggested and implemented. It based on optical-geometric approach, which is developed by the authors in recent years and previously used only for packing circles of equal radius. The results of computational experiment are presented and discussed.
The paper deals with approaches to heterogeneous data cleanse in processes of their preparation to integration. This process allows identifying and fixing different inconsistencies and errors in data to improve data q...
详细信息
A spreadsheet is one of popular forms for presentation and transferring data of the same types. The area of using this kind of documents is very widespread. Extraction tables from spreadsheets and their understanding ...
详细信息
We consider a non-convex optimal impulsive control problem for nonlinear differential equations, driven by vector-valued Borel measures, under no commutativity assumptions of the Frobenius type. For this problem, we d...
详细信息
We consider a non-convex optimal impulsive control problem for nonlinear differential equations, driven by vector-valued Borel measures, under no commutativity assumptions of the Frobenius type. For this problem, we derive nonlocal necessary optimality conditions operating with a specific class of impulsive feedback controls, generated by certain functions of the Lyapunov type. These feedback controls are constructed in a way similar to the dynamical programming, but with the use of weakly monotone solutions to the corresponding Hamilton-Jacobi equation, instead of the Bellman’s function. We offer the notion of weakly monotone function with respect to a measure-driven differential equation, and give constructive criteria for this type of monotonicity. Based on a space-time representation of impulsive processes, we propose the concept of impulsive feedback control and present nonlocal necessary optimality conditions, which are shown to filter out non-optimal extrema of the impulsive Maximum Principle.
暂无评论