Bojenje grafa primjenom logičke zadovoljivosti

undergraduate thesis

• Title (english): Graph Colouring with SMT Solver
• Author: Ivan Nizić
• Mentor: Bruno Blašković (mentor)
• Committee member: Bruno Blašković (predsjednik povjerenstva)
• Committee member: Mirko Randić (član povjerenstva)
• Committee member: Frano Škopljanac-Mačina (član povjerenstva)
• Granter: University of Zagreb; Faculty of Electrical Engineering and Computing; Zagreb
• Defense date and country: 2024-07-12, Croatia
• Scientific / art field, discipline and subdiscipline: TECHNICAL SCIENCES; Computing

Abstract

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.

Abstract (english)

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.

• Keywords: Programiranje s ograničenjima; Zadovoljivost; Yices; Bojanje grafa; Sudoku
• Keywords (english): Constraint programming; Satisfiability; Yices; Graph coloring; Sudoku
• Language: croatian
• URN:NBN: urn:nbn:hr:168:088005
• Study programme: Title: Computing; Study programme type: university; Study level: undergraduate; Academic / professional title: sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva (sveučilišni/a prvostupnik/ prvostupnica (baccalaureus/baccalaurea) inženjer/inženjerka računarstva)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Closed access
• Created on: 2024-10-12 21:41:43