Automated Reasoning, A.A. 2023/24

THU 10:30-12:30, room A036
FRI 12:30-14:30, room A036
(general material and references HERE)


  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.


  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.
``Recent'' work of the CLPLAB on Constraint and Logic Programming. Some slides of the "recent" presentations of the works at meetings.
Home Page