Referativn� semin�� o �e�en� probl�m� splnitelnosti. Hlavn� n�pln� semin��e budou modern� algoritmick� techniky pro �e�en� probl�m� booleovsk� splnitelnosti (SAT) a probl�m� spl�ov�n� podm�nek (CSP). Koncepty SAT a CSP p�edstavuj� d�le�it� n�stroje pro �e�en� slo�it�ch �loh v um�l� inteligenci. Na semin��i se mimo jin� se pod�v�me na: symetrie, konzistence, glob�ln� podm�nky jednotkov� propagace, filtrace, sledov�n� liter�l�, u�en� modern� SAT �e�i�e - MiniSAT, zChaff, PicoSat, RSAT modelov�n�: kombinatorick� �lohy, pl�nov�n� atd.

�as od �asu se bude semin�� konat v po��ta�ov� laborato�i, kde budeme prov�d�t experimenty s nastudovan�mi technikami.

Rozvrh: letn� semestr, 0/2 Z st�eda 15:40 - 17:10 S8/SU1 (za��n� se 23.2.2011 v SU1)
�mluva: Ji� prob�hla.

Plak�t semin��e (reklama na �mluvu)  [PDF]   |   Semin�� v SISu

---

Na rozmy�lenou: Pokuste se naj�t �tverec celo��seln�ho obsahu, kter� lze rozd�lit na n�kolik r�zn�ch men��ch �tverc� rovn� celo��seln�ho obsahu (viz. obr�zek v��e). Navrhn�te program, kter� by �lohu dok�zal vy�e�it. ��ste�n� �e�en� �lohy lze nal�zt na plak�tu k semin��i.

---

Zat�m zn�m� program

• 23.2.2011: Praktick� semin�� - organizace, soute�e v SATu
• 2.3.2011: Radek Mi�ek - SAT �e�i�e zalo�en� na DPLL [PDF]; Andrej Chovanec - Lok�ln� techniky: ESG, SAPS
• 9.3.2011: Praktick� semin�� - gener�tor mal�ch obt�n�ch formul�

Vytvo�en� k�d z 9.3.2011 hardgen-0.01.tgz: Rozpracovan� gener�tor (t�k�ch) formul� zalo�en� na genetick�m programov�n�.

• 16.3.2011: Martin Babka - (4/3)ⁿ algoritmus pro splnitelnost [PDF]
• 23.3.2011: Praktick� semin�� - pokra�ov�n� s gener�torem mal�ch obt�n�ch formul�

Vytvo�en� k�d z 23.3.2011 a pozd�ji hardgen-0.02.tgz: Nov� verze gener�toru (t�k�ch) formul� vyu��vaj�c�ho genetick� programov�n�. Pozn.: Je pot�eba opravit zav�r�ni soubor�. Konr�tn� soubor fitness.cnf je nutn� zav��t d��ve ne� je zavol�n MiniSat. hardgen-0.03.tgz: Opraveno zav�r�n� soubor� a generov�n� nov� populace, jako fitness se m�sto po�tu rozhodnut� pou��v� po�et propagac� kombinovan� s po�tem klauzul� (zat�m je pou�ita st�le jen mutace, k��en� je�t� pou�ito nen�).

• 30.3.2011: Tom� Balyo - Paraleln� algoritmy pro SAT
• 6.4.2011: Praktick� semin�� - pokra�ov�n� s gener�torem mal�ch obt�n�ch formul�

Vytvo�en� k�d z 6.4.2011 a pozd�ji hardgen-0.04.tgz: Nov� verze gener�toru (t�k�ch) formul� vyu��vaj�c�ho genetick� programov�n�. Nyn� jsou implementov�ny v�echny pot�ebn� vlastnosti, tj. mutace a k��en�. Mo�no d�le experimentovat s fitness funkc�. Pozn.: K�d odpov�d� p�esn� stavu na konci semin��e. hardgen-0.05.tgz: Verze s vylep�enou fitness funkc�. Bere se v �vahu po�et propagac� a po�et rozhodnut�, fitness funkce se m�rn� dynamicky adaptuje. hardgen-0.11.tgz: Fitness je nyn� vektor hodnot (po�et konflikt�, po�et rozhodnut�, ...), p�i�em� nejd�le�it�j�� slo�kou je po�et konflikt�. Plus mnoho dal��ch drobn�ch vylep�en�.

• 13.4.2011: Odpadne - konference
• 20.4.2011: Praktick� semin�� - Tom� Balyo - Jazyk pro formule; Martin Babka - Lloydova 15-ka; a dal��
• 27.4.2011: Andrej Chovanec - ILP - Inductive Logic Programming
• 4.5.2011: Praktick� semin��
• 11.5.2011: Tom� �apka - SAT Preprocessing [PDF]
• 18.5.2011: Odpadne - rektorsk� den
• 25.5.2011: Odpadne - konference