Bojenje grafa primjenom logičke zadovoljivosti

završni rad

• Naslov (engleski): Graph Colouring with SMT Solver
• Autor: Ivan Nizić
• Mentor: Bruno Blašković (mentor)
• Član povjerenstva: Bruno Blašković (predsjednik povjerenstva)
• Član povjerenstva: Mirko Randić (član povjerenstva)
• Član povjerenstva: Frano Škopljanac-Mačina (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Fakultet elektrotehnike i računarstva; Zagreb
• Datum i država obrane: 2024-07-12, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: TEHNIČKE ZNANOSTI; Računarstvo

Sažetak

Rad daje uvide u različite alate programiranja s ograničenjima i zadovoljivosti. Alati koji su predstavljeni uključuju CP, SAT, SMT te kao primjer SMT-a pomagalo Yices. Pomagalo Yices je ja također korišteno kod programskog dijela rada. Definiran je i glavni problem kojim se rad bavi, a to je bojanje vrhova grafa. Prikazano je i kako se taj problem rješava primjenom pojedinog alata programiranja s ograničenjima i zadovoljivosti. Igra Sudoku je korištena za ilustraciju problema bojanja grafa. Bojanje vrhova grafa različitim bojama se uspoređuje s popunjavanjem Sudoku tablice različitim brojevima. Programski dio rada u tu svrhu rješava zadanu Sudoku tablicu koristeći SMT pristup, odnosno Yices pomagalo.

Sažetak (engleski)

This paper provides an insight into constraint programming and satisfiability solvers. Those solvers include CP, SAT, SMT (Satisfiability Modulo Theories) and Yices solver, as an example of a SMT solver. Yices solver is also used in the practical part of the paper. The main problem presented in the paper is graph coloring. There are examples of how that problem is solved using each of the solvers above. The Sudoku game is used to explain the main problem of graph coloring. The problem of deciding which color to use on which point is compared to deciding which number to put in which cell of the Sudoku table. The practical part of the paper for that reason solves given Sudoku table by using the SMT solver Yices.

• Ključne riječi: Programiranje s ograničenjima; Zadovoljivost; Yices; Bojanje grafa; Sudoku
• Ključne riječi (engleski): Constraint programming; Satisfiability; Yices; Graph coloring; Sudoku
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:168:088005
• Studijski program: Naziv: Računarstvo; Vrsta studija: sveučilišni; Stupanj studija: preddiplomski; Akademski / stručni naziv: sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva (univ.bacc.ing.comp.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Zatvoreni pristup
• Datum i vrijeme pohrane: 2024-10-12 21:41:43