Course Work contains 2 homeworks and references
The goal: Using theorem provers to solve constraint satisfaction problems.
Language: SMT2 ("Satisfiability modulo theories"), Matlab
Introduction: The problem of determining whether there exists an interpretation that satisfies a given sentence in propositional logic is called as Satisfiability Problem (SAT). The variables of a given boolean formula are consistently assigned to the values TRUE or FALSE, to see whether there is any assignment that makes the formula to evaluate to TRUE. In that case the formula is called satisfiable. If there is no possible assignments that makes the formula true, then it is unsatisfiable.
Outputs:
- Matlab Scripts (.m)
- 3-SAT Problem Generator
- N-Queens SAT Problem Generator
- Scheduling Constraint Satisfiability Problem (CSP) Generator
- Specialized for Real Time Programming
- SAT problems (.txt and .smt2)
- Solutions to SAT problems (.txt)
The goal: In this assignment you will learn how to model and solve planning problems.
Language: PDDL ("Planning Domain Definition Language")
Introduction: PDDL (the "Planning Domain Definition Language") was designed to standardise planning domain and problem description languages for the International Planning Competitions (IPL). It is based on the STRIPS language developed Stanford Research Institute (SRI) to be used in Shakey the Robot. Besides STRIPS, PDDL contains features from ADL and more. You will need only the STRIPS subset of PDDL in this homework.
There are many planners available. Some recent planners are given in https://ipc2018.bitbucket.io/
In this homework you will use a planner that is accessible on http://editor.planning.domains/.