Automated Reasoning, A.A. 2024/25

Program

1. 30/09/2025. Course Introduction. The role of Automated Reasoning in AI. From 1955 to 2025. Remarks on course/exam. The notion of CSP and of COP (and their equivalence). Search space and naive search techniques. NP hardness of CSP solving.
2. 3/10/2025. SAT Encoding for solving CSP. DIMACS format. Examples of encoding (Rooks, Telethon, N-Queens, Sudoku). SAT solving. Unit propagation and DPLL. Use MiniSAT or clingo as a SAT solver. Sudoku solved by SAT as a sat solver (example of instance).
3. 7/10/2025. Constraint solving. Constraint rewriting rules. Proof rules: domain reduction rules, Transformation, and introduction rules. Derivation and constraint propagation. Node consistency. Arc consistency. Propagation stress using Minizinc.
4. 14/10/2025. Bounds Consistency. Directional Arc/Bounds Consistency. Hyperarc (and Bounds) consistency. Path Consistency.
   
5. 17/10/2025. Constrained Search: prop labeling trees. Introduction to MINIZINC. Basic search heuristics. Search meta-heuristics. FlatZinc.
6. 21/10/2025. Minizinc modeling: general ideas. Examples: Minizinc model of N-Queens. Minizinc modeling. Compiling to FlatZinc. Schur Numbers (Ramsey) problems. Some alphametic problems, Exercises.
7. 24/10/2025. Latin and Magic Squares, Sudoku. Timetabling: two general approaches. Telethon. Hamming codes: breaking symmetries. Knapsack. School Scheduling.
8. 27/10/2025. Solving COPs. The branch and bound in CP. Meta heuristics in constraint programming. Large Neighbourhood Search. Constraint Based Local Search.
   Extra material Two examples from Biology: Haplotype Inference and (simplified) Protein Folding.
9. 31/10/2025. 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. Exercises.
10. 4/11/2025. Brief historical introduction to AI, Automated Reasoning, and Logic Programming.
11. 7/11/2025. Practical lesson on Programming in Minizinc (exercises for students)
12. 11/11/2025. Syntax of Logic Programming: terms, atoms, rules. Intuitive semantics of rules. Logic Programs. ``finite world'' programs and infinite programs. Examples in Prolog.
13. 14/11/2025. Semantics of Logic (Programming). Universes, Interpretations, Models, Logical Consequences. Herbrand models. Intersection properties. Monotonicity and Continuity of TP. The Minimum model MP of Definite Clause Programs.
14. 18/11/2025. Computing MP.
    Top down. SLD resolution. Unification. (Operational Semantics of Prolog)
15. 21/11/2025. Computing MP.
    Bottom up. Fixpoint general results. Minimum and Maximum fixpoint of the TP operator. (Denotational Semantics of Logic Programming)
16. 24/11/2025. General programs. The loss of monotonicity. Completion of a general program and its Herbrand models. 3-valued semantics. The notion of stable model. Examples.
17. 25/11/2025. 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. Solvers.
18. 28/11/2025. 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,
19. 02/12/2025. Encoding CSP with ASP: Magic Square, Sudoku, Hamming Codes, University Timetabling, friendly football Tournament, Haplotype inference, Protein Structure Prediction.

    The part below is just a draft

20. 05/12/2024. Commonsense reasoning. An introduction by Baral and Gelfond. Automated reasoning with ASP. The zebra puzzle, "jobs puzzle", Smullyan's logic puzzles.
21. 09/12/2024. "Planning" puzzles. Wolf-cabbage-goat puzzle, the three barrels, the Hanoi Tower, Lloyd's puzzle, and other games. (ASP encodings)
22. 12/12/2024. KR languages, expressivity and complexity. Definitite, General, Disjunctive programs. The notions of Stable model and the complexity ot establishing their existence.
23. 19/12/2024. Programming in ASP (exercises for students - 3 hours)
24. 09/01/2024. 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. The language B and its encoding in ASP and in SAT/Constraint Programming. Multiagent planning. Centralized, Distributed, Epistemic.
25. 13/01/2024. ASP SOLVING. A quick view inside ASP solvers. Loop formulas and Nogoogds. Unfounded Sets. Clause Learning basics. Backjumping.
26. Inductive reasoning: ILP
Brave, cautious and probabilistic reasoning.

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