|
|
Classes of Boolean Formulae with Effectively Solvable SAT
Vlček, Václav ; Čepek, Ondřej (advisor) ; Kullmann, Oliver (referee) ; Savický, Petr (referee)
The thesis studies classes of Boolean formulae for which the well-known satisfiability problem is solvable in polynomially bounded time. It focusses on classes based on unit resolution; it describe classes of unit refutation complete formulae, unit propagation complete formulae and focuses on the class of SLUR formulae. It presents properties of SLUR formulae as well as the recently obtained results. The main result is the coNP-completness of membership testing. Finally, several hierarchies are built over the SLUR class and their properties and mutual relations are studied. Powered by TCPDF (www.tcpdf.org)
|
|
|
Structured problems for SAT
Klátil, Jan ; Hric, Jan (advisor) ; Kučera, Petr (referee)
Title: Structured problems for SAT Author: Jan Klátil Department: Department of Theoretical Computer Science and Mathematical Logic Supervisor: RNDr. Jan Hric, Department of Theoretical Computer Science and Mathematical Logic Abstract: Aim of this thesis is to implement generator of unstructured data of CSP model RB in format XCSP and several other generators of structured data in formats XCSP and DIMACS, which are based on problems of placing N-Queens, finding Hamiltonian cycle and dividing set of integers into two distinct subsets with equal sum. We compare generated data in both XCSP and DIMACS format based on same problem by comparing time spent by SAT solver RSAT solving this data. Both forced satisfiable and unsatisfiable data and joined unstructured a structured data in XCSP format were compared in this thesis. Keywords: structured problems, SAT 1
|
|
|
Planning algorithms and plan simulation in logistics domain
Štefan, Zdeněk ; Toropila, Daniel (advisor) ; Valla, Tomáš (referee)
The goal of this thesis is to compare some means of planning in the logistics domain.The aim was to compare the capabilities of those techniques among each other and against plans designed by humans.Because some planners do not return parallel plans,it is necessary to parallelize them.It is shown that some algorithms achieve good results in comparison to plans designed by hu- mans. However, due to their high time and memory consumptions they cannot be nowadays commonly used to solve more difficult tasks.
|
|
|
DPLL algorithm and propositional proofs
Hrnčiar, Maroš ; Krajíček, Jan (advisor) ; Koucký, Michal (referee)
Proof complexity is an interesting mathematical part connecting logic and complexity theory. It investigates which proof systems are needed for effective theorem proving. The aim of this paper is to present a relation between propositional proof systems and SAT algorithms. We will see that a run of an algorithm on the unrealizable formula can be seen as a propositional proof of its unsatisfiability, so the algorithm practically defines whole proof system. The thesis is mainly recommended for readers interested in proof complexity, but it can also independently illustrate a resolution principle and perhaps show some less common view of SAT assuming reader's basic knowledge of propositional logic, graph theory and complexity.
|
|
|
Collision Detection Library
Chlubna, Tomáš ; Španěl, Michal (referee) ; Polok, Lukáš (advisor)
This thesis deals with the problem of detecting collisions of nontrivial polygonal models in three-dimensional space. In general, there are methods describing how to mathematically express and calculate such collisions. However, such methods are usually unsuitable for usage in information technology due to the performance and memory requirements. It is also necessary to work with the discrete time that is not present in the real world. That brings the need to implement algorithms that are not only able to detect the collisions in a specific point in time, but also to predict them according to the available data about the movement of the objects in the scene. The solution uses game development and physics simulations techniques. Therefore, this works describes some optimization techniques as well as suitable scene representation formats and GPU rendering mechanisms.
|
|
|
GPU Accelerated SAT Solver
Izrael, Petr ; Šimek, Václav (referee) ; Jaroš, Jiří (advisor)
This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as well as the CUDA platform and a list of common algorithms used for solving the boolean satisfiability problem (the SAT problem). The presented solution is based on the 3-SAT DC alogirthm, which belongs to the family of well-known DPLL based algorithms. This work describes problems encountered during the design and implementation. The resulting application was then analyzed and optimized. The presented solver cannot compete with state of the art solvers, but proves that it can be up to 21x faster than an equivalent sequential version. Unfortunately, the current implementation can only handle formulas of a limited size. Suggestions on further improvements are given in final sections.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Magnetic fields for biomedical experiments
Otýpka, Jan ; Cipín, Radoslav (referee) ; Patočka, Miroslav (advisor)
In this work deals with magnetic fields for use in biomedicine. This solution involves the choice of the correct geometric arrangement of coils for generating magnetic field with a homogeneous distribution of magnetic induction of the widest possible area. The paper compares thre traditional types of coils, solenoid, toroid and Helmholtz coil. For Helmholtz and solenoid coil and is then carried out an analysis of the magnetic flux density in the inner space. Next part is devoted to electrical resonance in the LC circuit. This is then utilized for the development of pulsed magnetic field in the Helmholtz coil. It summarizes the theoretical and practical knowledge to design and construction of resonant converters. The end is devoted to the measurement of circuit parameters and verification of theoretical knowledge.
|
|
| |
|
| |
guest ::
