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ó.
Objectius:
- Introduir l'estudiant a la utilització d'eines basades en la lògica per a la modelització i resolució de problemes complexos, com ara problemes de planificació, scheduling (planificació del temps i els recursos), optimització, verificació de hardware i software, etc.
Habilitats:
- Ser capaç d'escollir les tècniques i eines de programació més adients per resoldre un problema, tant pel que fa al nivell d'expressivitat de la lògica subjacent com de la complexitat del problema deductiu associat.