Automated Reasoning, A.A. 2016/2017

Timetable

TUE 10:30-12:15, room 48
WED 10:30-12:15, room 22
(general material and references HERE) In case of missing files go to the page of the most recent edition of the course.

Program

  1. 28/09/2016. Course Introduction. CSP/COP and their equivalence. NP hardness of CSP. Search space and naive search techniques. (SLIDES)
  2. 29/09/2016. Survey on Local Search and (Integer) Linear Programming for solving COP and CSP. (SLIDES) Implementation of the naive techniques in Prolog (Prolog encoding).
  3. 05/10/2016. Execution of naive search. Motivation lectures By Peter Stuckey and by By Pascal Van Hentenryck. SAT solving. Examples of encoding. DIMACS format. Using clingo as a SAT solver. Sudoku solved by SAT as a sat solver (example of instance). (SLIDES)
  4. 06/10/2016. SAT solving: Davis Putnam (Logemann Loveland), Unit progagation, etc.

    Constraint Solving. Complete adn Incomplete Constraint Solvers. Proof rules: domain reduction, transformation and introduction. Derivation and constraint propagation. Node consistency. (SLIDES) Examples shown using the constraint solver of B-Prolog.

  5. 12/10/2016. Arc consistency. Bounds Consistency. Directional Arc/Bounds Consistency. Hyperarc (and Bounds) consistency. Path Consistency. (SLIDES)
  6. 13/10/2016. Constrained Search: prop labeling trees. Minizinc (download the tutorial). Simple examples. (SLIDES Minizinc model of N-Queens.)
  7. 19/10/2016. Some Minizinc modelings. SEND+MORE=MONEY, WRONG+WRONG=RIGHT (alphametic problems), Latin Square and Magic Square, Schur Numbers (Ramsey) problem. (Minizinc Models)
  8. 26/10/2016. Minizinc modeling. Sudoku, Knapsack, Hamming codes, Timetabling, TSP. (SLIDES and Minizinc Models)
  9. 27/10/2016. (Cumulative) Scheduling. Two examples from Biology: Haplotype Inference and (simplified) Protein Folding. (SLIDES and Minizinc Models)
  10. 02/11/2016. Global constraints. Hyper arc consistency and its asymptotical complexity. All different constraints. Bipartite Graph and matchings. Berge and Regin Theorems. Polynomial propagation of the alldifferent constraint. (SLIDES)
  11. 03/11/2016. Global constraints catalog. Approximated search with constraints. Large Neighborhood search. (SLIDES) Examples using BProlog Code.
  12. 09/11/2016. Historical Introduction to Logic Programming for Knowledge Representation and Reasoning. Syntax of Logic Programming: terms, atoms, rules. (SLIDES)
  13. 10/11/2016. Logic Programs. ``finite world'' programs and infinite programs. Examples in Prolog. Semantics of Logic (Programming). Universes, Interpretations, Models, Logical Consequences. (SLIDES)
  14. 16/11/2016. Herbrand models. Minimum model of Definite Clause Programs. Denotational Semantics. Minimum and Maximum fixpoint of the TP operator. (SLIDES)
  15. 17/11/2016. General programs. The loss of monotonicity. Completion of a general program and its Herbrand models. The notion of stable model. Examples. NP completeness main result. (SLIDES)
  16. 23/11/2016. ASP solving pipeline and main solvers. Grounding. Domain predicates. Intervals, Cardinality Constraints, and Aggregates Encoding CSP with ASP: magic square. (SLIDES)
  17. 24/11/2016. Encoding CSP with ASP: N-Queens, k-coloring, Schur Numbers, Hamilton Circuit, Hamming codes. (SLIDES, and ASP encodings)
  18. 30/11/2016. Encoding CSP with ASP. Sudoku, Telethon schedule, Football Tournament, Haplotype inference, Protein Structure Prediction (SLIDES).
  19. 07/12/2016. Commonsense reasoning. Automated reasoning with ASP: wolf-cabbage-goat puzzle, the zebra puzzle, the three barrels. (SLIDES).
  20. 14/12/2016. Talk by Alice Tarzariol on "Automated Reasoning applied to Biomedical Datasets" and by Davide Liessi on "Approaches to platform-based system synthesis with answer set programming" (SLIDES).
  21. 15/12/2016. Representing and solving the Hanoi Tower, Lloyd's puzzle, and other games. Representing ans solving Smullyan's logic puzzles (ASP encodings). ASP solving in brief. (SLIDES).
  22. 21/12/2016. Action Description Languages. The language B, its semantics, and its encoding in constraint programming and in ASP. PDDL. (SLIDES, the B to ASP translator. For other material, see This page and in particular, This one)
  23. 11/01/2017. KR languages, expressivity and complexity. (SLIDES)
  24. 12/01/2017. Report on recent work of the CLPLAB on Constraint and Logic Programming. Discussion about the exam (see the SLIDES).
Some slides of the "recent" presentations of the works at meetings.