National Repository of Dissertations in Serbia
    • English
    • Српски
    • Српски (Serbia)
  • English 
    • English
    • Serbian (Cyrilic)
    • Serbian (Latin)
  • Login
View Item 
  •   NaRDuS home
  • Универзитет у Београду
  • Математички факултет
  • View Item
  •   NaRDuS home
  • Универзитет у Београду
  • Математички факултет
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Rešavanje problema CSP tehnikama svođenja na problem SAT

Solving of constraint satisfaction problems by reduction to SAT

Thumbnail
2016
Disertacija.pdf (1.936Mb)
IzvestajKomisije8382.pdf (137.0Kb)
Author
Stojadinović, Mirko S.
Mentor
Marić, Filip
Committee members
Janičić, Predrag
Mitić, Nenad
Nikolić, Mladen
Vujošević, Mirko
Metadata
Show full item record
Abstract
Mnogi realni problemi se danas mogu predstaviti u obliku problema zadovoljenja ogranicenja (CSP) i zatim rešiti nekom od mnogobrojnih tehnika za rešavanje ovog problema. Jedna od tehnika podrazumeva svođenje na problem SAT, tj. problem iskazne zadovoljivosti. Promenljive i ogranicenja problema CSP se prevode (kodiraju) u SAT instancu, ona se potom rešava pomocu modernih SAT rešavaca i rešenje se, ako postoji, prevodi u rešenje problema CSP. Glavni cilj ove teze je unapređenje rešavanja problema CSP svođenjem na SAT. Razvijena su dva nova hibridna kodiranja (prevođenja u SAT formulu) koja kombinuju dobre strane postojecih kodiranja. Dat je dokaz korektnosti jednog od kodiranja koji do sada nije postojao u literaturi. Razvijen je sistem meSAT koji omogucava svođenje problema CSP na SAT pomocu cetiri osnovna i dva hibridna kodiranja, kao i rešavanje problema CSP svođenjem na dva problema srodna problemu SAT, SMT i PB. Razvijen je portfolio za automatski odabir kodiranja/rešavaca za ulaznu... instancu koju je potrebno rešiti i pokazano je da je razvijeni portfolio uporediv sa najefikasnijim savremenim pristupima. Prikazan je novi pristup zasnovan na kratkim vremenskim ogranicenjima sa ciljem da se znacajno smanji vreme pripreme portfolija. Pokazano je da se ovim pristupom dobijaju rezultati konkurentni onima koji se dobijaju korišcenjem standardnog vremena za pripremu. Izvršeno je poređenje nekoliko tehnika mašinskog ucenja, sa ciljem da se ustanovi koja od njih je pogodnija za pristup sa kratkim treniranjem. Prikazan je jedan realan problem, problem raspoređivanja kontrolora leta, kao i tri njegova modela. Veliki broj metoda rešavanja i raznovrsnih rešavaca je upotrebljeno za rešavanje ovog problema. Razvijeno je više optimizacionih tehnika koje imaju za cilj pronalaženje optimalnih rešenja problema. Pokazuje se da je najefikasnija hibridna tehnika koja kombinuje svođenje na SAT i lokalnu pretragu. Razmotren je i problem sudoku, kao i postojece tehnike rešavanja sudoku zagonetki vecih dimenzija od 9 x 9. Pokazuje se da je u rešavanju ovih zagonetki najefikasnije vec postojece svođenje na SAT. Unapređen je postojeci algoritam za generisanje velikih sudoku zagonetki. Pokazano je da jednostavna pravila preprocesiranja dodatno unapređuju brzinu generisanja sudokua.

Many real-world problems can be modeled as constraint satisfaction problems (CSPs) and then solved by one of many available techniques for solving these problems. One of the techniques is reduction to SAT, i.e. Boolean Satisfiability Problem. Variables and constraints of CSP are translated (encoded) to SAT instance, that is then solved by state-of-the-art SAT solvers and solution, if exists, is translated to the solution of the original CSP. The main aim of this thesis is to improve CSP solving techniques that are using reduction to SAT. Two new hybrid encodings of CSPs to SAT are presented and they combine good sides of the existing encodings. We give the proof of correctness of one encoding that did not exist in literature. We developed system meSAT that enables reduction of CSPs to SAT by using 4 basic and 2 hybrid encodings. The system also enables solving of CSPs by reduction to two problems related to SAT, SMT and PB. We developed a portfolio for automated selection of encoding/s...olver to be used on some new instance that needs to be solved. The developed portfolio is comparable with the state-of-the-art portfolios. We developed a hybrid approach based on short solving timeouts with the aim of significantly reducing the preparation time of a portfolio. By using this approach, we got results comparable to the ones obtained by using preparation time of usual length. We made comparison between several machine learning techniques with the aim to find out which one is the best suited for the short training approach. The problem of assigning air traffic controllers to shifts is described and three models of this problem are presented. We used a large number of different solving methods and a diverse set of solvers for solving this problem. We developed optimization techniques that aim to find optimal solutions of the problem. A hybrid technique combining reduction to SAT and local search is shown to be the most efficient one. We also considered sudoku puzzles and the existing techniques of solving the puzzles of greater size than 9x9. Amongst the used techniques, the existing reduction to SAT is the most efficient in solving these puzzles. We improved the existing algorithm for generating large sudoku puzzles. It is shown that simple preprocessing rules additionally improve speed of generating large sudokus.

Faculty:
Универзитет у Београду, Математички факултет
Date:
13-10-2016
Projects:
  • Automated Reasoning and Data Mining (RS-174021)
Keywords:
CSP / CSP / SAT kodiranje / portfolio / kontrolor / raspored / sudoku / SAT encoding / portfolio / air traffic controler / schedule / sudoku
[ Google Scholar ]
Handle
https://hdl.handle.net/21.15107/rcub_nardus_8000
URI
https://nardus.mpn.gov.rs/handle/123456789/8000
http://eteze.bg.ac.rs/application/showtheses?thesesId=4888
https://fedorabg.bg.ac.rs/fedora/get/o:15317/bdef:Content/download
http://vbs.rs/scripts/cobiss?command=DISPLAY&base=70036&RID=48835599

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS
 

 

Browse

All of DSpaceUniversities & FacultiesAuthorsMentorCommittee membersSubjectsThis CollectionAuthorsMentorCommittee membersSubjects

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS