Splnitelnost aritmetických formulí a Gröbnerovy báze
| Thesis title in Czech: | Splnitelnost aritmetických formulí a Gröbnerovy báze |
|---|---|
| Thesis title in English: | Satisfaction of arithemtical formulas and Gröbner bases |
| Academic year of topic announcement: | 2010/2011 |
| Thesis type: | diploma thesis |
| Thesis language: | |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | doc. RNDr. David Stanovský, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 29.09.2010 |
| Date of assignment: | 07.10.2010 |
| Guidelines |
| Tématem práce je tzv. SMT, satisfaction modulo theories, což je rozšíření známého problému SAT o proměnné, funkce a predikáty z nějaké nadstavbové teorie, typicky nějakého fragmentu aritmetiky. Konkrétně nám půjde o základní aritmetiku nad celými a reálnými čísly. Typická úloha může vypadat např. takto: existuje x:integer a b,c:boolean takové, že (b | x*x<0) & x!=0 & (~b | c | x=0) ?
K dispozici je řada SMT-solverů, tedy programů které řeší SMT, pro různé aritmetické teorie. Všechny jsou založeny na nějaké formě klasického DPLL algoritmu pro řešení SAT, rozšířeného o výpočty nad danou teorií. Cílem práce bude implementovat SMT-solver pro celočíselnou a reálnou aritmetiku, který převede zadání na soustavu polynomiálních rovnic nad daným číselným oborem, a tuto soustavu vyřeší pomocí Gröbnerových bází. SMT-solver bude implementován v systému Sage, který má řadu nástrojů pro symbolické výpočty a programovací jazyk na bázi jazyka Python. SMT-solver bude testován na benchmarkových úlohách z databáze SMT-LIB. Žádné speciální znalosti předem nejsou potřeba. Student bude muset nastudovat teorii řešení soustav polynomiálních rovnic, základy práce v systému Sage, knihovnu SMT-LIB. |
| References |
| D. Stanovský, Počítačová algebra, skripta v přípravě
http://www.smtlib.org http://www.sagemath.org John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge Uni. Press, 2009. |