Wyniki wyszukiwania - Biblioteka Nauki

1

On Fast Heuristic Non-deterministic Algorithms and Short Heuristic Proofs

100%

Itsykson D. , Sokolov D.

|

tom Vol. 132, nr 1

113--129

EN

In this paper we study heuristic proof systems and heuristic non-deterministic algorithms. We give an example of a language Y and a polynomial-time samplable distribution D such that the distributional problem (Y, D) belongs to the complexity class HeurNP but Y ∉ NP if NP ≠ coNP, and (Y, D) ∉ HeurBPP if (NP, PSamp) ⊆ HeurBPP. For a language L and a polynomial q we define the language padq (L) composed of pairs (x, r) where x is an element of L and r is an arbitrary binary string of length at least q(|x|). If D = {Dn}∞ n=1 is an ensemble of distributions on strings, let D × Uq be a distribution on pairs (x, r), where x is distributed according to Dn and r is uniformly distributed on strings of length q(n). We show that for every language L in AM there is a polynomial q such that for every distribution D concentrated on the complement of L the distributional problem (padq (L), D × Uq) has a polynomially bounded heuristic proof system. Since graph non-isomorphism (GNI) is in AM, the above result is applicable to GNI.

2

Analysis of Static Data Flow Structures

80%

Sokolov D. , Poliakov I. , Yakovlev A.

|

2008

|

tom Vol. 88, nr 4

581-610

EN

A token-based model for asynchronous data path, called static data flow structures (SDFS), is formally defined. Three token game semantics are introduced for this model, namely atomic token, spread token and counterflow. The SDFS semantics are analysed using a simple benchmark example; their advantages and drawbacks are highlighted. A combination of spread token and counterflow models, which employs the advantages of both, is presented. A technique is described for mapping the high-level SDFS token game semantics into the low level of underlying Petri nets (PNs). The PNs are employed as a back-end for verification of SDFS models. For analysis and comparison of SDFS semantics a software tool has been developed, which integrates all SDFS semantics into a consistent framework, implements their conversion into PNs and provides an interface to existing model checking tools.

3

Tight Lower Bounds on the Resolution Complexity of Perfect Matching Principles

80%

Itsykson D. , Slabodkin M. , Oparin V. , Sokolov D.

Fundamenta Informaticae

|

2016

|

tom Vol. 145, nr 3

229--242

EN

The resolution complexity of the perfectmatching principle was studied by Razborov [1], who developed a technique for proving its lower bounds for dense graphs. We construct a constant degree bipartite graph Gn such that the resolution complexity of the perfect matching principle for Gn is 2Ω(n)) where n is the number of vertices in Gn. This lower bound is tight up to some polynomial. Our result implies the 2Ω(n) lower bounds for the complete graph K2n+1 and the complete bipartite graph KnO(n), that improves the lower bounds following from [1]. We show that for every graph G with n vertices that has no perfect matching there exists a resolution refutation of perfect matching principle for G of size O(n22n). Thus our lower boundsmatch upper bounds up to a multiplicative constant in the exponent. Our results also imply the well-known exponential lower bounds on the resolution complexity of the pigeonhole principle, the functional pigeonhole principle and the pigeonhole principle over a graph. We also prove the following corollary. For every natural number d, for every n large enough, for every function h : {1, 2, . . . , n} → {1, 2, . . . , d}, we construct a graph with n vertices that has the following properties. There exists a constant D such that the degree of the i-th vertex is at least h(i) and at most D, and it is impossible to make all degrees equal to h(i) by removing the graph's edges. Moreover, any proof of this statement in the resolution proof system has size 2Ω(n). This result implies well-known exponential lower bounds on the Tseitin formulas as well as new results: for example, the same property of a complete graph. Preliminary version of this paper appeared in proceedings of CSR-2015 [2].

4

Substantiation of the choice of the cutter material and method of its hardening, working under the action of friction and cyclic loading

80%

Sokolov D. , Sobyna V. , Vambol S. , Vambol V.

|

tom Vol. 94, nr 2

49--54

EN

Purpose: The main problem with the use of rescue instruments during emergency response is the low strength of the tool’s cutting edge. The consequence of this is the low efficiency of rescue operations. The purpose of this study is to substantiate experimentally the choice of material for the tool’s cutting edge and the method of surfacing it on the cutter of a hydraulic tool, operating under the simultaneous influence of friction and cyclic loading. Design/methodology/approach: The choice of material was carried out by the way of analytical analysis with subsequent experimental verification. For this purpose, specially made samples of cutters from various grades of alloyed steel were used. With these cutters the steel rod Ø 12 mm made of St3 steel was cut; the number of cutting cycles preceding blunting or destruction of the cutting edge of the tool was counted. Analytical study of the possibility of cutter’s surface hardening by fusing the cutting edge onto it was carried out by the way of analyzing scientific research in the area of improving the technical characteristics of a mechanized hydraulic tool. Findings: It has been experimentally established that Steel 30HGT gives the greatest number of working cycles before blunting, while steels of the manufacturer (Steel 65G and Steel 12M) are destroyed in 180 and 200 working cycles, respectively. Other steels are not destroyed, but can stand fewer number of cutting cycles. To reduce the cost and increase the efficiency of rescue operations, it is proposed to perform surface hardening of the tool cutter by fusing the cutting edge made of Steel 30 HGT steel (analogs: in Germany – 30MnCrTi; in the Czech Republic – 14231). Analytical research has shown that manual arc welding as a method of welding metals is widely tested, reliably reproducible, allows for surfacing in any conditions outside the fabrication facility and is carried out with non-bulky equipment. This will increase the life of the hydraulic rescue tool. Research limitations/implications: The study was conducted for steels that meet the requirements of national standards. Practical implications: Equipping rescue workers with a mechanized tool that has been upgraded by the proposed method improves the efficiency of rescue operations in emergency situations. Originality/value: It is proposed to increase the strength and reliability of a mechanized tool for rescue operations. For the first time, an attempt to substantiate the choice of method for hardening the cutting) edge of an instrument by applying reliably reproducible technologies was made.

5

Experimental investigation and modelling of austenite microstructure evolution processes occurring in line-pipe steels under hot rolling

70%

Rudskoy A. I. , Vasilyev A. , Kolbasnikov N. , Sokolov S. , Sokolov D.

Hutnik, Wiadomości Hutnicze

|

2011

|

tom Vol. 78, nr 5

415--420

EN

An experimental study of the processes of austenite microstructure evolution occurring under hot rolling was performed for line-pipe steels with different chemical composition. All investigations were conducted with the help of the Gleeble 3800 system. Empirical quantitative models of austenite grain growth, static and dynamic recrystallization, as well as a flow stress model were developed. The effect of complex alloying by such elements as C; Mn; Si; Ni; Mo; Nb; Ti; and V on grain growth and recrystallization is accounted for under the condition that all elements are in a solid solution.

PL

W pracy przedstawiono badania eksperymentalne ewolucji ziarna austenitu zachodzącej podczas walcowania na gorąco w stalach o zróżnicowanym składzie chemicznym, przeznaczonych na rurociągi dużych średnic. Wszystkie badania wykonano za pomocą systemu Gleeble3800. Opracowano empiryczne ilościowe modele rozrostu ziarna austenitu, statycznej i dynamicznej rekrystalizacji, jak również model naprężenia uplastyczniającego. Wpływ dodatków stopowych pierwiastków: C; Mn; Si; Ni; Mo; Nb; Ti i V na rozrost ziarna i rekrystalizację uwzględniono przy założeniu, że wszystkie dodatki znajdują się w roztworze stałym.

6

Persistent and Nonviolent Steps and the Design of GALS Systems

61%

Fernandes J. , Koutny M. , Mikulski Ł. , Pietkiewicz-Koutny M. , Sokolov D. , Yakovlev A.

Fundamenta Informaticae

|

2015

|

tom Vol. 137, nr 1

143--170

EN

A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in a single clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. In this paper, we move to the realm of step based execution and consider not only steps which are persistent and cannot be disabled by other steps, but also steps which are nonviolent and cannot disable other steps. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundled steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps.