1. Introducció i motivació.
1.1. Alguns exemples de problemes. Com els resoldríem amb les tècniques vistes a assignatures prèvies? Quant de temps ens costaria? Què en sabríem de les garanties de fiabilitat?
2. Classes de complexitat i reduccions.
2.1. Algunes classes importants: P, NP, ...
2.2. Reduccions.
2.3. Problemes NP-complets i NP-hard.
2.4. Alguns problemes NP-hard: Programació entera, Pseudo-booleans (0-1 integer programming), 3-SAT, ...
3. Recordatori de lògica proposicional i de lògica de primer ordre.
3.1. Sintaxi i semàntica.
3.2. Resolució.
4. Programació lògica amb restriccions (Constraint Logic Programming)
4.1. Repàs de Prolog.
4.2. CLP(X) i dominis.
4.3. Maneres de reduir l'espai de cerca.
4.4. Exemples: assignació de recursos, horaris, ...
4.5. Cerca de solucions òptimes amb CLP.
5. Tècniques basades en SAT.
5.1. Sistemes DPLL amb anàlisi de conflictes.
5.2. Programació per traducció a SAT i ús de les eines associades.
5.3. Exemples d'aplicacions: problemes d'horaris, etc.
5.4. Extensions: Max-SAT, All-SAT.
6. SAT mòdul teories (SMT).
6.1. SMT amb arrays, llistes, enters i reals.
6.2. Reduccions a SAT. Mètodes eager.
6.3. Mètodes lazy. DPLL(T).
7. Comparació amb altres tècniques.
7.1. SAT i Integer Programming (IP).
7.2. SAT i Constraint Programming (CP).
7.3. Aplicació de SMT a CSPs i problemes combinatoris d'optimització.
8. Aplicacions. Alguns àmbits de possible aplicació d'aquestes tècniques.
8.1. Verificació de circuïts.
8.2. Verificació de protocols criptogràfics.
8.3. Representació de sistemes d'estats finits.