Computer Science
Recent Submissions
-
Banković, Milan (Beograd , 2016)[more][less]
Abstract: SMT solvers implement decision procedures that check for satisfiability of first-order logical formulae with respect to some decidable theory. They rely on the powerful techniques that are used for solving boolean satisfiability problem (SAT), combined with specific procedures that permit reasoning in a particular theory. Typical applications of SMT solvers are mostly found in software verification, and for this reason the theories frequently considered in SMT solvers are best suited for such kind of applications. Extending the applicability of SMT solvers to other areas may require defining new SMT theories, as well as developing the corresponding decision procedures for such theories. In that sense, in this thesis we consider improving of SMT solvers by extending their applicability to solving CSP problems. Such problems consider variables with finite domains, and the goal is to find the assignment of values to the variables of the problem satisfying all the imposed constraints. When CSP solving is considered, the main drawback of the existing SMT theories is that they are not adapted to the problems with finite domains, and are also incapable of reasoning about global constraints, which play the significant role in most CSP problems. For this reason, in this thesis a novel SMT theory is defined that enables natural representation of CSP problems, since it includes support for some frequently used global constraints. For such theory, we developed a decision procedure based on the existing techniques borrowed from the traditional CSP solvers, but these techniques are adapted in the way that permits their usage within SMT solvers. The decision procedure currently supports two types of global constraints: the alldifferent constraint and the linear constraint. In case of the alldifferent constraint, the main contribution is a novel algorithm for generating explanations of conflicts and propagations, which is required for the conflict analysis. In case of the linear constraint, a novel filtering algorithm is developed that takes into consideration the existence of the alldifferent constraints in the given problem, which can lead to a stronger propagation. Another direction of improving SMT solvers that is considered in the thesis is the usage of the parallelization techniques. We consider the parallelization of the simplex algorithm, which is used in SMT solvers as the decision procedure for the linear arithmetic. We also consider the parallel portfolio approach, as well as the hybridization of the two approaches. A comprehensive experimental evaluation is provided on a large number of instances, both industrial and randomly generated. For the purpose of all the mentioned research, during the work on the thesis a new open-source SMT solver called argosmt is developed, based on DPLL(T ) architecture. URI: http://hdl.handle.net/123456789/5835 Files in this item: 1
Disertacija_8.pdf ( 2.359Mb ) -
Šandrih, Branislava (Beograd , 2020)[more][less]
Abstract: The main goal of this dissertation is to put different text classification tasks in the same frame, by mapping the input data into the common vector space of linguistic attributes. Subsequently, several classification problems of great importance for natural language processing are solved by applying the appropriate classification algorithms. The dissertation deals with the problem of validation of bilingual translation pairs, so that the final goal is to construct a classifier which provides a substitute for human evalu- ation and which decides whether the pair is a proper translation between the appropriate languages by means of applying a variety of linguistic information and methods. In dictionaries it is useful to have a sentence that demonstrates use for a particular dictio- nary entry. This task is called the classification of good dictionary examples. In this thesis, a method is developed which automatically estimates whether an example is good or bad for a specific dictionary entry. Two cases of short message classification are also discussed in this dissertation. In the first case, classes are the authors of the messages, and the task is to assign each message to its author from that fixed set. This task is called authorship identification. The other observed classification of short messages is called opinion mining, or sentiment analysis. Starting from the assumption that a short message carries a positive or negative attitude about a thing, or is purely informative, classes can be: positive, negative and neutral. These tasks are of great importance in the field of natural language processing and the proposed solutions are language-independent, based on machine learning methods: sup- port vector machines, decision trees and gradient boosting. For all of these tasks, a demonstration of the effectiveness of the proposed methods is shown on for the Serbian language. URI: http://hdl.handle.net/123456789/5801 Files in this item: 1
Disertacija.pdf ( 9.053Mb ) -
Veljković, Aleksandar (Beograd , 2023)[more][less]
Abstract: Bioinformatics as a science of the future faces the problems of processing a large amount of data that is increasing every day. In addition to the problem of data storage, the challenge is also data analysis and the understanding of hidden relations between biological entities that are observed only after unifying data from different data sources. This thesis proposes a novel data model for the unification of heterogeneous data from multiple bioinformatics databases and a system architecture design for implementing software systems based on the proposed data model. Additionally, the thesis defines an automated pipeline for discovering new semantic similarity relations based on data mining methods using the data found in the proposed data model. The data model, software architecture, and automatic pipeline are evaluated using data from five real-world bioinformatics databases. The results demonstrate a high flexibility of the data model and the high efficiency of the software system implemented following the proposed architecture design. URI: http://hdl.handle.net/123456789/5794 Files in this item: 1
Disertacija_15649.pdf ( 2.864Mb ) -
Carić, Marko (Beograd , 2023)[more][less]
Abstract: In this dissertation, the problem of calculating the number of equiva- lence classes of Boolean functions is discussed. The difficulty of determining the number of equivalence classes increases sharply with the number of variables n. The motivation for choosing this topic lies in the fact that concrete numbers have been known so far only for relatively small values of n, although the problem itself was theoretically solved a long time ago. Let G be the group of permutations of the set Bn = {0, 1}n. The effect of the group G on scalar, Bn 7 → B1, that is, vectorial invertible Boolean functions, Bn 7 → Bn. Two scalar Boolean functions f (x) and g(x), defined on Bn, are considered equivalent with respect to the group G, i.e. f ∼ g, if for some σ ∈ G for every x ∈ Bn f (x) = g(σ(x)) holds. Two vector invertible Boolean functions f (x) and g(x), are considered equivalent with respect to the group G, i.e. f ∼ g, if for some pair (σ, ρ) ∈ G × G for each x ∈ Bn holds g(x) = ρ(f (σ(x))). The equivalence relation ∼ decomposes the set of all Boolean functions into equivalence classes. Equivalence of Boolean functions has significant applications in the logical synthesis of combinatorial circuits and in cryptography, especially in connection with the design of S-boxes. Let Un(G) and Vn(G) denote number of equivalence classes of scalar, i.e. vector invertible Boolean functions of n variables in relation to the group G. The numbers Un(G) and Vn(G) can be calculated relatively simply if the cycle index of the group G is known. The dissertation considers four groups G of permutations of the set Bn: • group S′ n induced by group Sn permutations of coordinates elements x = (x1, x2, . . . , xn) ∈ Bn, • group Gn, induced by permutations and complementations of coordinates, • group of GLn linear invertible transformations elements of the vector space Bn, i • group of AGLn affine invertible transformations elements Bn. If the permutation σ ∈ G has ik cycles of length k ⩾ 1, its cycle structure is i(σ) = (i1, i2, . . .). The cyclic index of the group G is the generatrix ZG(f1, f2, . . .) = 1 |G| X σ∈G Y k⩾1 f ik k of cycle structures of all permutations σ ∈ G. General expressions for cycle indices the four considered groups are known, but the cycle indices themselves, i.e. the numbers Un(G) and Vn(G), are practically calculated only for relatively small values, for e.g. n ⩽ 10. The dissertation presents original results in the field of enumeration of equiv- alence classes of Boolean functions in relation to these four groups of transfor- mations. A similar expression was derived for all four groups of transformations for the cycle index in the form of sum over partitions of the number n. Based on that expression and previously calculated tables, the cycle index is calculated much more efficiently. An overview of known results for relatively small n and new results in the thesis for larger n is shown in the following table: Number\ G S′ n Gn GLn AGLn Un(G) 11 → 33 10 → 32 8 → 31 10 → 31 Vn(G) 6 → 30 7 → 27 6 → 26 6 → 26 Specially, in the case of the permutation group S′ n, an effective direct procedure for calculating the number of equivalence classes that does not use a cycle index is shown, and is described in the third paper from the introductory chapter. The second part of the dissertation concerns monotone Boolean functions — scalar Boolean functions which satisfy the monotonicity condition (from x ⩽ y follows f (x) ⩽ f (y)). Let rn, i.e. dn (the n-th Dedekind number), denote the number of equivalence classes of monotone Boolean functions in relation to the group S′ n, that is, the total number of monotone Boolean functions of n variables. The difficulty of calculating the number rn increases rapidly with n, so that until recently the last calculated member of the sequence was r7. The procedure described in the dissertation is based on the Frobenius theorem, by which it was determined number r8. In doing so, the known value of the number d8 is used. The dissertation consists of the first - introductory chapter and the following three chapters. In the second chapter, theoretical terms related to the material from chapters 3 and 4 are introduced, and they refer to discrete mathematics, combinatorics and cycle indices of the considered four groups of transformations. Chapter 3 describes the procedure for calculating the cycle indices for the four considered groups of permutations, as well as numbers Un(G) and Vn(G) equivalence classes of Boolean functions in relation to these groups. First, common improvements for all four groups are considered, and then specific accelerations related to individual groups. These results are published in the second paper listed in the introductory chapter. In chapter 4, the problem of finding the number of equivalence classes of monotone Boolean functions is solved. First, a general expression for calculating the number rn is given based on the Frobenius theorem in the form of the sum (by partitions of the number n) of the number of fixed points of the permutation corresponding to the partition. After that, depending on the graphs corresponding to different partitions, different ways of calculating the number of fixed points for n ⩽ 8 are shown. The procedure based on which the number r8 was calculated, which also represents the original contribution of this dissertation is presented - see the first paper from the list from the introductory chapter. Applying a similar procedure, Pawelski [31] calculated r8 practically at the same time as the obtained result described in the dissertation. URI: http://hdl.handle.net/123456789/5792 Files in this item: 1
Disertacija_15671.pdf ( 2.414Mb ) -
Ristović, Ivan (Beograd , 2026)[more][less]
Abstract: Cloud-computing platforms provide services to consumers through multiple serviceoffering models. Recent advances in these models have led to the emergence of serverless computing, or simply serverless, where infrastructure is managed by the service provider. Serverless is usually coupled with function-based programming model in which software systems are composed of reusable, lightweight units of code executed within isolated sandboxed environments. Major cloud-computing platforms, including Amazon Web Services (AWS), Microsoft Azure, and Google Cloud, report that a substantial proportion of their customers employ serverless solutions. Most cloud-computing providers employ a pay-as-you-go billing model. Inefficient utilization of computing resources, particularly CPU time and working memory, which constitute the most costly resources, leads to increased overall operational costs. Moreover, the requirement for resource isolation adversely affects initialization latency and results in additional CPU and working-memory overhead. Serverless sandboxes are typically deployed on top of heavyweight virtualization stacks that includeJava, JavaScript, or Python runtime environments with accompanying frameworks, further increasing working-memory consumption. Modern cloud-computing architectures use Checkpoint/Restore (abbr. c/r) techniques to freeze initialized sandboxes into a continuable form. Such techniques, in combination with cloud-native deployments, allow the virtualized environment to optimize resource consumption and share code and pre-initialized data across multiple sandboxes. However, such solutions either operate at application-build time to support data pre-initialization or sharing, or operate at execution time with limited sharing potential for data available during application execution. Such data is processed multiple times and duplicated in each sandbox. This dissertation presents Doss, a direct object snapshotting and sharing system that performs data c/r during application execution. Doss persists data directly, without transformations, into reusable and shareable snapshots. Direct snapshotting allows Doss to achieve near-constant data deserialization time, greatly improving initialization times and reducing CPU usage. Doss architecture enables snapshot sharing across application instances, eliminating the excess memory footprint associated with data re-processing and duplication. GraalDoss, a Doss implementation for Java, is integrated into the GraalVM ecosystem. GraalDoss is evaluated using 106 correctness and robustness tests and a novel set of cloudnative micro and macro benchmarks that exercise real-world scenarios. A comprehensive evaluation of GraalDoss shows a consistent near-constant data-deserialization overhead with serialization times comparable to state-of-the-art Java JSON and binary serialization libraries. GraalDoss reduces the memory footprint of web API microservice caches by sharing populated cache snapshots across microservice instances, improving the overall density by 41% for 8 microservice instances and improving first-response times by 34%. In NLP applications, GraalDoss improves the pipeline execution times by six orders of magnitude by snapshotting pipeline results and subsequently loading the snapshots. URI: http://hdl.handle.net/123456789/5786 Files in this item: 1
IvanRistovic_PhD_Dissertation.pdf ( 4.683Mb )