Problem Solving and Constraint Programming (RPAR)

Fall Semester 2011

Professors

• Structure. The course will have three parts:
  • 1. Linear Programming (Enric Rodríguez; from 4/10 to 27/10)
  • 2. Boolean Satisfiability (Albert Oliveras; from 3/11 to 24/11)
  • 3. Constraint Programming (Javier Larrosa; from 29/11 to 12/1)
  
  
• Evaluation. There will be a practical work (50% of final grade) and a final exam (50% of final grade)


• Practical work.
  
• The practical work is due on January 19th.
  
• The description of the work is here. (updated Nov. 15th) Note: there was a typo in the definition of the at-most-one constraints. The order predicate should be <=.
  
• The set of instances is here.
  
• An example script for executing a set of instances with a time limit is available here.
• In Comet, you can abort an execution after n seconds with "cp.timeLimit(int n)".
  


• Final Exam. 
• The grades are here.
• The exam with solutions is here.
  
• We have decided to have the revision of the exam and the project simultaneously on January 23rd, from 12:00 to 13:00.
• The final exam will take place in the last lecture of the course, January 12th, starting at 8:30. You can take to the exam personal notes, class hand-outs, books, etc. Access to internet will NOT be permitted.
  
• You can find last year's exam here
  

• Session 1. Basics on Linear Programming
• Session 2. The Simplex Method
• Session 3. The Revised Simplex Method
• Session 4. The Dual Simplex Method
• Session 5. LP Solvers and Languages
• Session 6. Mixed Integer Linear Programming
• Session 7. Modeling and Solving Problems with Mixed Integer Programming


• LP Solvers:
• GLPK
• GLPK for Windows


• References:
• Maros István, Computational Techniques of the Simplex Method, Kluwer Academic Publishers
• Robert Vanderbei, Linear Programming: Foundations and Extensions, Springer
• H.P. Williams, Model Building in Mathematical Programming, Wiley

• Session 1. Quick introduction to Propositional Logic
• Session 2. The DPLL Algorithm
• Session 3. Resolution in Propositional Logic
• Sessions 4 and 5. Encoding Problems in Propositional Logic
• Sessions 6 and 7. From DPLL to CDCL SAT solvers
• Session 8. Extracting proofs from CDCL SAT solvers.
• Session 9. An Introduction to SMT.


• SAT Solvers:
• MiniSAT
• PrecoSAT


• References:
• Chaff: Engineering an Efficient SAT Solver
• Conflict driven learning in a quantified Boolean Satisfiability solver
• Solving SAT an SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) (Sections 1 and 2)
• Handbook of Satisfiability. IOS Press

• Session 1. Basic Definitions
• Session 2. Basic Modeling with Comet
• Session 3. Local Consistency
• Session4. Global Constraints I and II
• Session 5. Tuning the Search
  


• References:
• Handbook of Constraint Programming. Elsevier (Chapters 3 and 6)
• Comet Reference book