Projet Programmation Logique 2015

Prolog

• PDF (Prolog exercises)
• ZIP (quelques solutions)

Deadlines

• Submitting the SAT/SMT project (by mail): May 20
• Soutenance for SAT/SMT project: May 22

Links

• Prolog (Wikipedia)
• GProlog manual (HTML)
• GProlog manual (PDF)

SAT/SMT solving

• The first part of the subject: PDF (SAT solving)
• The second part of the subject: PDF (SMT solving)
• Examples: ZIP (updated 12/02)
• Some additional examples: ZIP
• Puzzle Generators: ZIP
• Package for graphical output: ZIP
• Frontend for SAT solving with Z3: ZIP
• Solver plus puzzle generators: ZIP (new 22/04)

Deadlines

• Submitting the SAT/SMT project (by mail): March 4
• Soutenance for SAT/SMT project: March 6

Links

• Z3 solver - direct link to Tutorial
• Reflex (Flash game)
• Wikipedia page on SMT (gives an overview of the topic with links to quite a few papers and tools)
• Satisfiability Solvers (Survey in the Handbook of Knowledge Representation)
• Basics of SAT Solving Algorithms (slides presenting common techniques used in SAT solvers)
• A Declarative Encoding of Telecommunications Feature Subscription in SAT (paper explaining how to encode acyclicity in SAT, see Section 5)
• A New SAT Encoding of the At-Most-One Constraint (paper surveying methods to encode at-most-one constraints)

Enseignants: Stefan Schwoon, Lucca Hirschi