Na t�to str�nce budou postupn� zve�ej�ov�na t�mata, ze kter�ch je mo�n� vyb�rat refer�ty na semin��. Ke ka�d�mu t�matick�mu okruhu jsou uvedeny �l�nky, ze kter�ch je mo�n� �erpat. Zat�m je zde v�ce k booleovsk� splnitelnosti (SAT), omezuj�c� podm�nky (CSP) jsou tak� zastoupeny, ale sp�e v souvislosti se SATem.

Zp�sob referov�n� bude dohodnut na semin��i, nicm�n� standardn� se p�edpokl�d�, �e ka�d� student odreferuje dva a� t�i odborn� �l�nky. Inovac� oproti klasick�m referativn�m semin���m bude praktick� �e�en� n�jak� �lohy pomoc� nastudovan�ch technik. C�lem semin��e nen� odreferovat co nejv�ce t�mat, ale hloub�ji pochopit zaj�mav� techniky.

�l�nky k t�mat�m zde nejsou on-line, proto�e by to odporovalo autorsk�m pr�v�m. Av�ak v�echny �l�nky je mo�n� vyhledat a voln� st�hnout (pozn.: z fakultn�ch po��ta�� je p��stup i do v�t�iny on-line �asopis�, kter� voln� p��stupn� nejsou).

---

V�eobecn� �vod k SATu
Definice probl�mu booleovsk� splnitelnosti, z�kladn� �e��c� techniky (DPLL, heuristiky, jednotkov� propagace - unit propagation). Z�ejm� p�ednesu s�m, aby v�ichni ��astn�ci m�li spole�n� z�kladn� znalosti, kter� budou pot�eba k dal��m t�mat�m.

• Anbulagan, Jussi Rintanen: SAT: Algorithms and Applications


• Jussi Rintanen: Reasoning about dynamic systems by satisfiability testing: planning, diagnosis and model-checking

U�en� v SATu
U�en� se z konflikt� nalezen�ch b�hem prohled�v�n� prostoru �e�en�.

• Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver


• Paul Beanie, Henry Kautz, Ashish Sabharwal: Understanding the Power of Clause Learning
• Joao P. Marques Silva, Karem A. Sakallah: GRASP � a new search algorithm for satisfiability

Konzistence v SATu
Aplikace technik vyvinut�ch pro spl�ov�n� probl�m� s podm�nkami (CSP - constraint satisfaction problems) v SATu. Konziste�n� techniky umo��uj� probl�m zjednodu�it. Probl�mem z�st�v� pom�r v�po�etn� slo�itosti konzistence a m�ra zjednodu�en� probl�mu (Skute�n� u�et��me �as?).

• Ian P. Gent: Arc Consistency in SAT


• Christian Bessire, Emmanuel Hebrard, Toby Walsh: Local consistencies in SAT

Struktura probl�mu
Re�ln� �lohy modelovan� jako probl�m SAT se typicky vyzna�uj� v�ce �i m�n� z�etelnou strukturou. Znalost takov� struktury umo��uje v�razn� zmen�en� prohled�van�ho prostoru. P�edstavme si nap��klad, �e probl�m je jak�msi zp�sobem symetrick�, pak symetrick� �e�en� nen� nutn� uva�ovat.

• Armin Biere, Carsten Sinz: Decomposing SAT Problems into Connected Components


• Eyal Amir, Sheila McIlraith: Solving Satisfiability using Decomposition and the Most Constrained Subproblem


• Ines Lynce and Joao Marques-Silva: Hidden Structure in Unsatisfiable Random 3-SAT: an Empirical Study


• Fadi A. Aloul, Arathi Ramani, Igor L. Markov and Karem A. Sakallah: Solving Difficult SAT Instances in the Presence of Symmetry


• Alasdair Urquhart: Hard Examples for Resolution

Modelov�n� a transformace
Zaj�mavou ot�zkou jsou zp�soby modelov�n� konkr�tn� �lohy. R�zn� vztahy lze vyj�d�it mnoha ekvivalentn�mi zp�soby z nich� ka�d� je vhodn� pro jin� �e��c� techniky. Ot�zkou je tak� automatick� odvozov�n� ekvivalentn�ch model� a jejich propojov�n�.

• Alan M. Frisch, Ian Miguel, Toby Walsh: CGRASS: A System for Transforming Constraint Satisfaction Problems


• Toby Walsh: SAT vs. CSP

Inteligentn� prohled�vac� techniky
Inteligentn� prohled�vac� techniky zalo�en� na u�en� se z nalezen�ch konflikt�. Obecn�j�� pojedn�n� z pohledu omezuj�c�ch podm�nek. Pro SAT se pou��vaj� sp�e jednodu��� varianty. U slo�it�j��ch variant inteligentn�ho prohled�v�n� je ot�zkou efektivn� implementace.

• Andrew B. Baker: Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results


• Matthew L. Ginsberg: Dynamic backtracking


• Matthew L. Ginsberg: GSAT and Dynamic Backtracking


• William D. Harvey: Nonsystematic backtracking search

Implementa�n� techniky
Technick� t�ma. D�le�itou technikou pro n�vrh efektivn�ho �e��c�ho syst�mu pro SAT je tzv. sledov�n� liter�l�. Technika sledov�n� liter�l� umo��uje backtracking p�i �e�en� SATu s mal�mi n�klady.

• Lintao Zhang, Sharad Malik: The Quest for Efficient Boolean Satisfiability Solvers


• Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver

Lok�ln� techniky
Zaj�mav� t�ma p�edstavuj� techniky hled�n� spl�uj�c�ho ohodnocen�, pomoc� zlep�ov�n� �pln�ho ohodnocen� prom�nn�ch pomoc� lok�ln�ch zm�n.

• Bart Selman, Henry Kautz: Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems


• Henry Kautz, Bart Selman: Pushing the envelope: planning, propositional logic, and stochastic search


• A. Braunstein, M. M�zard, R. Zecchina: Survey propagation: An algorithm for satisfiability


• Dale Schuurmans, Finnegan Southey, Robert C. Holte: The Exponentiated Subgradient Algorithm for Heuristic Boolean Programming


• F. Hutter, D. Tompkins, H Hoos: Scaling and Probabilistic Smoothing: Efficient Dynamic Local Search for SAT

Konkr�tn� �e��c� syst�my pro SAT
P�ehledov� t�ma. Existuj�c� �e��c� syst�my pro SAT. Jejich srovn�n�, v�hody, nev�hody. Experiment�ln� v�sledky. Mezi zaj�mav� �e��c� syst�my pat�� MiniSAT, zChaff, RSat, PicoSAT, COMPSAT. Informace k jednotliv�m �e��c�m syst�m�m lze nal�zt na internetov�ch str�nk�ch autor� a na str�nk�ch sout�� SAT Competition a SAT Race.

Praktick� �lohy
Pokusme se namodelovat re�ln� probl�m jako SAT a vy�e�me jej pomoc� existuj�c�ho �e��c�ho syst�mu. Kter� �e�i� si povede nejl�pe? Jak� vliv bude m�t zp�sob modelov�n�? Konkr�tn� probl�my budou uvedeny pozd�ji, zat�m se zamysleme nad konstrukc� perfektn�ho �tverce (viz. plak�t semin��e).

• Ines Lynce, Joel Ouaknine: Sudoku as a SAT Problem