Semin�� ze splnitelnosti (NAIL092)
|
|
|
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:
|
�as od �asu se bude semin�� konat v po��ta�ov� laborato�i, kde budeme prov�d�t experimenty s nastudovan�mi technikami. Za�azen� experiment�ln� ��sti je u semin��e �pln� nov� p��stup, jsem p�esv�d�en, �e bude p��nosn�.
Rozvrh: letn� semestr 2009/2010, 0/2 Z, �ter� 9:00 - 10:30 S301/SU1 (za��n� se 2.3.2010 v S301)
�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
- 2.3.2010: Pavel Surynek - Probl�my SAT a CSP, z�kladn� �e��c� techniky pro SAT a CSP
- 9.3.2010: Praktick� �e�en� probl�m� (v laborato�i): Dimacs CNF form�t, Minisat
- 16.3.2010: Pavel Surynek - Lok�ln� techniky
- 23.3.2010: Praktick� �e�en� probl�m� (v laborato�i): rovnosti/nerovnosti pro bitov� vektory
- 30.3.2010: Pavel Surynek - Klikov� konzistence (semetrie se nestihly, budou jindy)
- 6.4.2010: Praktick� �e�en� probl�m� (v laborato�i): aritmetika pro bitov� vektory
- 13.4.2010: Adam Nohejl - Chaff: Engineering an Efficient SAT Solver
- 20.4.2010: Praktick� �e�en� probl�m� (v laborato�i): perfektn� �tverec
- 27.4.2010: Odpadne
- 4.5.2010: Praktick� �e�en� probl�m� (v laborato�i): dokon�en� perfektn�ho �tverce
- 11.5.2010: V�clav Vl�ek - Obt�n� instance SAT
- 18.5.2010: Praktick� �e�en� probl�m� (v laborato�i): pravd�podobn� lok�ln� techniky
|
Copyright © 2003-2014 Pavel Surynek |
|