Combinatorial Decision Making & Optimization

• Tools
  • MiniZinc：A modeling language with interfaces to several CP (and other) solvers (https://www.minizinc.org/).
  • Z3：A SAT/SMT solver (https://github.com/Z3Prover/z3/)

Syllabus

CONSTRAINT PROGRAMMING

• February 17: Introduction to the course and CP
• February 19: Modelling
• February 24: Local consistency, constraint propagation, global constraints
• February 26: Search
• March 3, 5: CP Exercises in MiniZinc (professor)

SAT

• March 10: Introduction to SAT, formula proof in SAT, encoding decision problems in SAT & basic solving techniques (resolution, unit propagation, DPLL)
• March 12: Conflict-driven clause learning SAT solvers, hybrid CP-SAT solving
• March 17: SAT encodings
• March 19, 24: SAT exercises in Z 3 (tutor)
• March 30 (aula 0.6 at 16:00): SAT exercises in Z 3 (tutor)
• March 31: More CP and SAT exercises (professor + tutor)

Exam

• A unique written exam (paper-based) for the entire course.
• An oral exam maybe required at the discretion of the lecturers.
• 4 sessions in July 7, September 11, January and February 2027.

每个 part 都有：

• 选择题
• Exercise：Show/Explain some examples