Automated Reasoning, A.A. 2022/23

BLENDED COURSE - MATERIAL ON MICROSOFT TEAMS

Program

1. 28/09/2022. 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. 30/09/2022. 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. 03/10/2022. 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. Examples.
4. 12/10/2021. Bounds Consistency. Directional Arc/Bounds Consistency. Hyperarc (and Bounds) consistency. Path Consistency.
   Constrained Search: prop labeling trees. Basic search heuristics.
5. 14/10/2022. Introduction to MINIZINC. Minizinc (download the tutorial). Example of constraint propagation in Minizinc. Minizinc modeling: general ideas. Examples: Minizinc model of N-Queens.
6. 19/10/2022. Minizinc modeling. Compiling to FlatZinc. Some alphametic problems, Latin and Magic Squares, Schur Numbers (Ramsey) problems, Sudoku.
7. 21/10/2022. Hamming codes: breaking symmetries. Solving COPs. The branch and bound in CP. Two (typical) encodings of Timetabling. School Scheduling.
   Extra material Two examples from Biology: Haplotype Inference and (simplified) Protein Folding.
8. 26/10/2022. 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.
9. 28/10/2022. Meta heuristics in constraint programming. Large Neighbour Search. Constraint Based Local Search. Intervento di Eugenia Zanazzo.
10. 02/11/2022. Brief historical introduction to AI, Automated Reasoning, and Logic Programming.
11. 04/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. 09/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. 11/11/2022. Computing MP.
    Top down. SLD resolution. Unification. (Operational Semantics of Prolog)
    Bottom up. Fixpoint general results. Minimum and Maximum fixpoint of the TP operator. (Denotational Semantics of Logic Programming)
14. 16/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.
15. 18/11/2022. 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.
16. 23/11/2022. Programming in ASP. Intervals, Cardinality Constraints, and Aggregates. Encoding CSP with ASP: N-Queens.
17. 25/11/2022. Encoding CSP with ASP: k-coloring, Telethon schedule, Schur Numbers, Hamilton Circuit, Magic Square, Hamming Codes, Sudoku, friendly football Tournament, Haplotype inference, Protein Structure Prediction. ASP encodings)
18. 07/12/2022. Commonsense reasoning. An introduction by Baral and Gelfond. Automated reasoning with ASP. The zebra puzzle, "jobs puzzle", Smullyan's logic puzzles.

    RESTO DEL CORSO ... DA SISTEMARE

19. 09/12/2022. "Planning" puzzles. Wolf-cabbage-goat puzzle, the three barrels, the Hanoi Tower, Lloyd's puzzle, and other games. (ASP encodings)
20. 13/12/2021. KR languages, expressivity and complexity. Definitite, General, Disjunctive programs. The notions of Stable model and the complexity ot establishing their existence.
21. 15/12/2021. Action Description Languages. Brief history. Syntax and semantics of the language B. Static and Dynamic causal laws. Examples
22. 20/12/2021. Complexity results: PSPACE Completeness of the Planning. The language B and its encoding in ASP and in SAT/Constraint Programming.
23. 22/12/2021. Multiagent planning. Censtralized, Distributed, Epistemic.
24. 10/01/2022. ASP SOLVING. A quick view inside ASP solvers. Clause Learning basics. Unfounded Sets. (lesson in collaboration with Andrea Formisano)

• 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)