Pavel Surynek's Academic Page | Semin�� ze splnitelnosti (NAIL092)

Semin�� ze splnitelnosti (NAIL092)

Obecn�  |  T�mata  |  Povinnosti     

Motivan� obr�zek

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�: diagnostika jako SAT, pl�nov�n� jako SAT, atd.

�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