| dc.contributor.advisor |
Marić, Filip |
|
| dc.contributor.author |
Banković, Milan |
|
| dc.date.accessioned |
2026-10-19T15:03:38Z |
|
| dc.date.available |
2026-10-19T15:03:38Z |
|
| dc.date.issued |
2016 |
|
| dc.identifier.uri |
http://hdl.handle.net/123456789/5835 |
|
| dc.description.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. |
en_US |
| dc.description.provenance |
Submitted by Slavisha Milisavljevic (slavisha) on 2026-10-19T15:03:37Z
No. of bitstreams: 1
Disertacija_8.pdf: 2359838 bytes, checksum: 75d1d1839954311440e7a6a839306841 (MD5) |
en |
| dc.description.provenance |
Made available in DSpace on 2026-10-19T15:03:38Z (GMT). No. of bitstreams: 1
Disertacija_8.pdf: 2359838 bytes, checksum: 75d1d1839954311440e7a6a839306841 (MD5)
Previous issue date: 2016 |
en |
| dc.language.iso |
sr |
en_US |
| dc.publisher |
Beograd |
en_US |
| dc.title |
UNAPREĐIVANJE SMT REŠAVAČA KORIŠĆENJEM CSP TEHNIKA I TEHNIKA PARALELIZACIJE |
en_US |
| mf.author.birth-date |
1982-05-03 |
|
| mf.author.birth-place |
Petrovac na Mlavi |
en_US |
| mf.author.birth-country |
Srbija |
en_US |
| mf.author.residence-state |
Srbija |
en_US |
| mf.author.citizenship |
Srpsko |
en_US |
| mf.author.nationality |
Srbin |
en_US |
| mf.subject.area |
Computer Science |
en_US |
| mf.subject.keywords |
computer science, automated reasoning, SAT solvers, SMT solvers, CSP solvers, parallelization |
en_US |
| mf.subject.subarea |
Automated reasoning |
en_US |
| mf.contributor.committee |
Živković, Miodrag |
|
| mf.contributor.committee |
Janičić, Predrag |
|
| mf.contributor.committee |
Ognjanović, Zoran |
|
| mf.university.faculty |
Mathematical Faculty |
en_US |
| mf.document.references |
105 |
en_US |
| mf.document.pages |
193 |
en_US |
| mf.document.location |
Beograd |
en_US |
| mf.document.genealogy-project |
No |
en_US |
| mf.university |
Belgrade University |
en_US |