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