Automated Reasoning, A.A. 2023/24

Program

1. 04/10/2023. Course Introduction. The role of knowlegde representation and problem solving in Artificial Intelligence. Remarks on course/exam. CSP/COP and their equivalence. NP hardness of CSP. Search space and naive search techniques.
2. 05/10/2023. SAT solving. Examples of encoding. DIMACS format. Use MiniSAT or clingo as a SAT solver. Sudoku solved by SAT as a sat solver (example of instance). Brief introduction to Local Search. Solving COPs with (Integer) Linear Programming.
3. 12/10/20222 SAT solving: unit propagation and DPLL: first example of constraint solver. Constraint solving. Constraint rewriting rules. Proof rules: domain reduction rules, Transformation, and introduction rules. Derivation and constraint propagation. Node consistency. Arc consistency.
4. 13/10/2023. Examples of arc consistency. Bounds Consistency. Directional Arc/Bounds Consistency. Hyperarc (and Bounds) consistency. Path Consistency.
   
5. 19/10/2023. Constrained Search: prop labeling trees. Basic search heuristics. Introduction to MINIZINC. Minizinc. Example of constraint propagation in Minizinc.
6. 20/10/2023. Minizinc modeling: general ideas. Examples: Minizinc model of N-Queens. Minizinc modeling. Compiling to FlatZinc. Schur Numbers (Ramsey) problems. Exercises.
7. 26/10/2023. Some alphametic problems, Latin and Magic Squares, Sudoku. Exercises. Hamming codes: breaking symmetries.
8. 27/10/2023. Solving COPs. The branch and bound in CP. Meta heuristics in constraint programming. Large Neighbour Search. Constraint Based Local Search. Knapsack. Two (typical) encodings of Timetabling. School Scheduling.
   Extra material Two examples from Biology: Haplotype Inference and (simplified) Protein Folding.
9. 02/11/2023. [on-line, due to meteo red alert] Global constraints. Hyper arc consistency and its asymptotical complexity. All different constraints. Bipartite Graph and matchings. Berge and Regin Theorems. Maximum matchings. Polynomial propagation of the alldifferent constraint. Global constraints catalog. TSP. (Cumulative) Scheduling.
10. 09/11/2022. Brief historical introduction to AI, Automated Reasoning, and Logic Programming.
11. 10/11/2022. Syntax of Logic Programming: terms, atoms, rules. Intuitive semantics of rules. Logic Programs. ``finite world'' programs and infinite programs. Examples in Prolog.
12. 16/11/2022. Semantics of Logic (Programming). Universes, Interpretations, Models, Logical Consequences. Herbrand models. Intersection properties. Monotonicity and Continuity of TP. The Minimum model of Definite Clause Programs.
13. 17/11/2022. Computing MP.
    Top down. SLD resolution. Unification. (Operational Semantics of Prolog)
14. 23/11/2022. Computing MP.
    Bottom up. Fixpoint general results. Minimum and Maximum fixpoint of the TP operator. (Denotational Semantics of Logic Programming)
15. 24/11/2022. General programs. The loss of monotonicity. Completion of a general program and its Herbrand models. 3-valued semantics. The notion of stable model. Examples.
16. 30/11/2023. Denials (ASP constraints). Encoding non-determinism. The problem of existence of a stable model. NP completeness main result. ASP solving pipeline and main solvers. Grounding. Domain predicates and range restrictedness.
17. 01/12/2023. Programming in ASP. Intervals, Cardinality Constraints, and Aggregates. Encoding CSP with ASP: N-Queens. Encoding CSP with ASP: k-coloring, Telethon schedule, Schur Numbers, Hamilton Circuit,
18. 07/12/2023. Encoding CSP with ASP: Magic Square, Sudoku, Hamming Codes, University Timetabling, friendly football Tournament, Haplotype inference, Protein Structure Prediction.
19. 14/12/2023. Commonsense reasoning. An introduction by Baral and Gelfond. Automated reasoning with ASP. The zebra puzzle, "jobs puzzle", Smullyan's logic puzzles.
20. 15/12/2023. "Planning" puzzles. Wolf-cabbage-goat puzzle, the three barrels, the Hanoi Tower, Lloyd's puzzle, and other games. (ASP encodings)
21. 21/12/2023. KR languages, expressivity and complexity. Definitite, General, Disjunctive programs. The notions of Stable model and the complexity ot establishing their existence.
22. 22/12/2024. ASP SOLVING. A quick view inside ASP solvers. Loop formulas and Nogoogds. Unfounded Sets. Clause Learning basics. Backjumping.

    DA SISTEMARE

23. 22/12/2023. Action Description Languages. Brief history. Syntax and semantics of the language B. Static and Dynamic causal laws. Examples Complexity results: PSPACE Completeness of the Planning.
24. 22/12/2024. The language B and its encoding in ASP and in SAT/Constraint Programming. Multiagent planning. Centralized, Distributed, Epistemic.

• Comparison between B/ASP and B/CLP and the BMV language
• Centralized Multiagent planning.
• Autonomous Multiagent Planning: BAAC.
• PDDL compilation in PICAT
• Exploiting the CUDA architecture:
  • A brief survey
  • for a SAT solver
  • for a constraint solver
  • for a ASP solver
• SOKOBAN and its B, BMV, and tabled prolog encoding.
  
• The solver GASP that delays the grounding.
• Protein Structure prediction using CLP(FD) and fragment assembly. ICLP 2010 (best paper).
• Logic programming and coinduction.
• Logic Programming and bisimulation.
• The role of SAT, CP, and LP in COmputational Biology (Invited Talk in Melbourne, 2017)
• GPU parallelism for ASP Solving (INAP 2019 - invited talk)
• 3COSOKU (CILC 2020 - best paper)
• Epistemic Planning in ASP (ICLP 2020)