DM850: Satisfiability (10 ECTS)

STADS: 15018401

Niveau
Kandidatkursus forhåndsgodkendt som PhD-kursus

Undervisningsperiode
Kurset er placeret i forårssemesteret.

Ansvarlige undervisere
Email: petersk@imada.sdu.dk

Skemaoplysninger
Vis hele skemaet
Vis personligt skema for dette kursus.

Kommentar:
Ubegrænset deltagerantal.

Indgangskrav:
Bestået bachelorgrad i datalogi, matematik, anvendt matematik, matematik-økonomi eller tilsvarende.

Faglige forudsætninger:
Studerende, der følger kurset, forventes at:

• have kendskab til basale begreb og koncepter vedr. udsagns logik og første ordens logik.
• kunne anvende basale transformationer af logiske udtryk samt ræsonnere vedr. sandhed af logiske formler.
• kunne vurdere kompleksitet af algoritmer, såvel med hensyn til køretid som med hensyn til pladsforbrug.

Formål
Kurset har til formål at sætte den studerende i stand til at anvende Satisfiability som metode til at løse beregningsmæssigt ikke-triviale problemer på en alligevel i praksis tit effektiv måde. Oversættelse af problemer til Satisfiability (både SAT og SMT) er blevet en standard metode i mange datalogiske områder, alt fra model checking til bioinformatik, således at kendskab til og kundskab i Satisfiability er relevant for en kandidat i datalogi.

Kurset bygger oven på den viden, der er erhvervet i kurserne DM549 Diskrete Metoder til Datalogi og DM552 Programmeringssprog. Ligeledes kan koncepter fra DM554 Kompleksitet og beregnelighed og DM554 Lineær og heltalsprogrammering finde anvendelse i kurset. Kurset giver et fagligt grundlag for at lave et speciale, hvor SAT eller SMT anvendes.

I forhold til uddannelsens kompetenceprofil har kurset eksplicit fokus på at:

• give kompetence til at planlægge og udføre videnskabelige projekter på højt fagligt niveau på baggrund af projekter baseret på videnskabelige artikler/bogkapitler.
• give færdigheder i udvikle nye varianter af de lærte metoder, hvor det konkrete problem kræver det på baggrund af den store båndbrede af emner afdækket af de videnskabelige artikler/bogkapitler.
• give færdigheder i at formidle forskningsbaseret viden og diskutere professionelle og videnskabelige problemstillinger på baggrund af de studenterledte seminarer.
• give viden om et udvalg af specialiserede modeller og metoder udviklet inden for datalogi baseret på højeste internationale forskning, herunder emner fra fagets forskningsfront på baggrund af udvalget af de videnskabelige artikler/bogkapitler.
• give viden om datalogiske modeller og metoder beregnet til anvendelser i andre faglige områder på baggrund af den store båndbrede af emner afdækket af de videnskabelige artikler/bogkapitler.
• give ekspertviden på et afgrænset fagområde, der er baseret på det højeste internationale forskningsfelt inden for det datalogiske fagområde på baggrund af underviserens aktive rolle i forskningsfeltet.

Målbeskrivelse
For at opnå kursets formål er det læringsmålet for kurset, at den studerende demonstrerer evnen til at:

• demonstrere grundlæggende viden om principperne og algoritmerne bag SAT og SMT løsere. 
• vurdere om en oversættelse til SAT eller SMT er en relevant metode til at løse et givet problem.
• forstå og derefter formilde såvel skriftligt som mundligt videnskabelige artikler/bogkapitler fra forskningsfeltet.
• anvende og overføre metoder fra de præsenterede anvendelser til nye problemer, også fra andre faglige kontekster.
• implementere løsninger til problemer baseret på en oversættelse til SAT eller SMT og anvende state-of-the-art SAT eller SMT løsere på resultatet.

Indhold
Kurset indeholder følgende faglige hovedområder:

• SAT problemet og triviale SAT løsere
• DPLL algoritmen og andre uundværlige komponenter af state-of-the-art SAT løsere
• SMT problemet og associerede teorier
• DPLL(T) algoritmen og eksempler af konkrete instanser 
• principper for effektive oversættelser til SAT
• koderingsmetoder for forskellige standardkonstruktioner
• anvendelser af SAT og SMT løsere til problemer fra forskellige områder

Litteratur

Meddeles ved kursets start.

Kursets hjemmeside
Dette kursus benytter e-learn (blackboard).

Forudsætningsprøver
Mundtlig fremlæggelse. Bestået/ikke-bestået, intern bedømmelse ved underviser. (15018412)

Eksamen- og censurform:
Projektopgave. Bedømmes efter 7-trinsskalaen, ekstern censur. (15018402)

Vejledende timetal
På naturvidenskab er undervisningen tilrettelagt efter trefasemodellen dvs. intro, trænings- og studiefasen.
Introfase: 28 timer
Træningsfase: 28 timer, heraf:
 - Eksaminatorie: 14 timer
 - Laboratorieøvelser: 14 timer

Aktiviteter i studiefasen

Undervisningsform
Undervisningen i introfasener opdelt i to dele. Den første del består af interaktive forelæsninge, der behandler de relevante principper. Den anden del består af seminarundervisning, hvor de studerende præsenterer og diskuterer på baggrund af tildelte videnskabelige artikler/bogkapitler vedr. forskellige applikationer.

Træningsfasen er opdelt i eksaminatorier, hvor stoffet og særligt de videnskabelige artikler/bogkapitler diskuteres, og laboratorieøvelser, hvor praktiske færdigheder i anvendelsen af relevante værktøjer øves.

Derudover anvendes det tilegnede viden i projekter, der udarbejdes i studiefasen. De videnskabelige kilder, der har dannet grundlag til seminarundervisning, og projektet bliver sammenfattet i et videnskabelig manuskript. I studiefasen arbejdes med: Anvendelse af det tilegnede viden i praktiske projekter, sammenfatning af tildelte videnskabelige artikler/bogkapitler og praktiske eksperimenter med de i kurset introducerede værktøjer.

Sprog
Dette kursus undervises på dansk eller engelsk, afhængigt af underviseren. Dog altid på Engelsk ved deltagelse af internationale studerende.

Kursustilmelding
Se tilmeldingsfrister.

Pris for åben uddannelse
Se priser for enkeltkurser.

Denne kursusbeskrivelse var gyldig fra 1. februar 2016 til 31. august 2019.