Show simple item record

Improving SMT solvers using CSP techniques and parallelization techniques

dc.contributor.advisorMarić, Filip
dc.contributor.otherŽivković, Miodrag
dc.contributor.otherJaničić, Predrag
dc.contributor.otherOgnjanović, Zoran
dc.creatorBanković, Milan M.
dc.date.accessioned2017-04-29T21:49:23Z
dc.date.available2017-04-29T21:49:23Z
dc.date.available2020-07-03T08:38:30Z
dc.date.issued2016-12-08
dc.identifier.urihttp://nardus.mpn.gov.rs/handle/123456789/7996
dc.identifier.urihttp://eteze.bg.ac.rs/application/showtheses?thesesId=4878
dc.identifier.urihttps://fedorabg.bg.ac.rs/fedora/get/o:15293/bdef:Content/download
dc.identifier.urihttp://vbs.rs/scripts/cobiss?command=DISPLAY&base=70036&RID=48837391
dc.description.abstractSMT решавачи имплементирају процедуре одлучивања за испитивање задовољивости логичких формула првог реда у односу на неку унапред задату одлучиву теорију. Ослањајући се на моћне технике за решавање проблема исказне задовољивости (SAT)у комбинацији са специфичним процедурама одлучивања које омогућавају резоновање у конкретној теорији. Типична примена SMT решавача је у верификацији софтвера, па су зато теорије које се стандарно користе у SMT решавачима прилагођене тој врсти примене ...sr
dc.description.abstractSMT 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
dc.formatapplication/pdf
dc.languagesr
dc.publisherУниверзитет у Београду, Математички факултетsr
dc.rightsopenAccessen
dc.sourceУниверзитет у Београдуsr
dc.subjectрачунарствоsr
dc.subjectcomputer scienceen
dc.subjectаутоматско резоновањеsr
dc.subjectSAT решавачиsr
dc.subjectSMT решавачиsr
dc.subjectCSP решавачиsr
dc.subjectпаралелизацијаsr
dc.subjectautomated reasoningen
dc.subjectSAT solversen
dc.subjectSMT solversen
dc.subjectCSP solversen
dc.subjectparallelizationen
dc.titleУнапређивање SMT решаваче коришћењем CSP техника и техника паралелизацијеsr
dc.title.alternativeImproving SMT solvers using CSP techniques and parallelization techniquesen
dc.typedoctoralThesis
dc.rights.licenseBY
dcterms.abstractМарић, Филип; Огњановић, Зоран; Живковић, Миодраг; Јаничић, Предраг; Банковић, Милан М.; Unapređivanje SMT rešavače korišćenjem CSP tehnika i tehnika paralelizacije;
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/6484/IzvestajKomisije8372.pdf
dc.identifier.fulltexthttp://nardus.mpn.gov.rs/bitstream/id/6483/Disertacija.pdf


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record