Automated Reasoning, A.A. 2021/22

BLENDED COURSE - MATERIAL ON MICROSOFT TEAMS

MON 10:30-12:30, room A025 / B01 since Oct 11
WED 8:30-10:30, room A025
(general material and references HERE)

Program

  1. 27/09/2021. Course Introduction. The role of knowlegde representation and problem solving in Artificial Intelligence. CSP/COP and their equivalence. NP hardness of CSP. Search space and naive search techniques.
  2. 30/09/2020. 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. 04/10/2021. 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. 6/10/2021. Bounds Consistency. Directional Arc/Bounds Consistency. Hyperarc (and Bounds) consistency. Path Consistency.
    Constrained Search: prop labeling trees. Basic search heuristics.
  5. 11/10/2021. Introduction to MINIZINC. Minizinc (download the tutorial). Example of constraint propagation in Minizinc. Minizinc modeling: general ideas. Examples: Minizinc model of N-Queens.
  6. 13/10/2021. Minizinc modeling. Compiling to FlatZinc. Some alphametic problems, Latin and Magic Squares, Schur Numbers (Ramsey) problems, Sudoku.
  7. 18/10/2021. Hamming codes: breaking symmetries. Solving COPs. The branch and bound in CP. Two (typical encodings) of Timetabling.
  8. 20/10/2021. Two examples from Biology: Haplotype Inference and (simplified) Protein Folding.
  9. 25/10/2021. 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. 27/10/2021. Brief historical introduction to AI, Automated Reasoning, and Logic Programming.
  11. 04/11/2020. Syntax of Logic Programming: terms, atoms, rules. Intuitive semantics of rules. Logic Programs. ``finite world'' programs and infinite programs. Examples in Prolog.
  12. 8/11/2021. Semantics of Logic (Programming). Universes, Interpretations, Models, Logical Consequences. Herbrand models. Intersection properties. The Minimum model of Definite Clause Programs.
  13. 10/11/2021. 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. 17/11/2021. General programs. The loss of monotonicity. Completion of a general program and its Herbrand models. 3-valued semantics. The notion of stable model. Examples. Denials (ASP constraints).
  15. 22/11/2021. 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. 24/11/2021. Programming in ASP. Intervals, Cardinality Constraints, and Aggregates. Encoding CSP with ASP: N-Queens, k-coloring, Telethon schedule, Schur Numbers, Hamilton Circuit ASP encodings)
  17. 29/11/2021. Meta heuristics in constraint programming. Large Neighbour Search. Constraint Based Local Search.
  18. 01/12/2021. Encoding CSP with ASP: Magic Square, Hamming Codes, Sudoku, friendly football Tournament, Haplotype inference, Protein Structure Prediction.
  19. 06/12/2021. Commonsense reasoning. An introduction by Baral and Gelfond. Automated reasoning with ASP. The zebra puzzle, "jobs puzzle", Smullyan's logic 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)
``Recent'' work of the CLPLAB on Constraint and Logic Programming. Some slides of the "recent" presentations of the works at meetings.
Home Page