Algoritmide ja andmestruktuuride erikursus
|
Course code: ITI8590 |
Time and place
Lectures: every Monday at 10:00-11:45 at ICT403
Practice sessions: Mondays at 14:00, in room 411
Learning outcomes
In Estonian:
- teab mitmete erialgoritmide tööpõhimõtteid
- on suuteline rakendama neid algoritme erinevate ülesannete lahendamiseks
- teab mitmete andmestruktuuride tööpõhimõtteid ja on suuteline neid rakendama
- suudab analüüsida järjestikuste ja rekursiivsete algoritmide keerukust
Brief description of the course
The course focuses on the internals of the methods of automated reasoning:
- The main bulk of the course: algorithms and data structures used for full first order (FOL) reasoners.
- The latter part will be extended to algorithms and data structures for extending standard FOL reasoners to the tasks of commonsense reasoning.
- We will also have a look at:
- Solving propositonal formulae
- SMT methods
Course materials
Will be given during the course. Materials are either presentations for specific methods or scientific papers covering such methods.
- An introductory material to field is the set of course notes from Geoff Sutcliffe.
- A simpler introduction in Estonian book chapter pages 297-345 by Tanel Tammet.
- The second most important material is course notes by Stephan Schulz: this concerns implementation aspects.
- In case you want to see a highly theoretical intro to the field, check out Christoph Weidenbach's coursebook
Practice work
Will contain all of these:
- Writing problem converters
- Writing small, toy prover components
- Experimenting with automated reasoning systems on specific problem sets
Practice work 1
Get some provers running (at least two, but more is better!):
- Go check the current top provers for the First-order Theorems division of the latest casc competition. You may want to have a brief look at short system descriptions.
- Download and install at least Vampire (the overall top prover) and GKC (the new prover by T.Tammet, targeting large problems)
- Download and unpack TPTP problem set: here is the direct download link).
- Have a quick look at the TPTP technical manual
- Try to get the PyRes running: this is a pedagogical prover in Python by Stephan Schulz.
You may also run these on dijkstra like this:
ssh kasutajanimi@dijkstra.cs.ttu.ee
Practice work 2
Familiarize yourself with the provers:
- Run Vampire and GKC on some smaller problems in TPTP: start with initial problems from the PUZ domain (puzzles) and then the KRS domain (knowledge representation). Read the output and understand the basics.
- Encode some small problems from the Tammet book chapter or Sutcliffe material and run the provers on these. Read the output and undestand the basics.
Practice work 3
Do some excercises and exam style questions from the first chapters of the Sutcliffe tutorial (select yourself some from the excercizes and exam style questions)
Practice work 4
Build a script to run both Vampire and GKC on the TPTP KRS domain, considering only problems ending with +*.p like KRS119+1.p:
- Find if there are any provable problems Vampire fails on in 30 seconds, list these.
- Find if there are any provable problems GKC fails on in 30 seconds, list these.
NB! A significant percentage of the problems in KRS are known to be not provable: these have the Status line value as either CounterSatisfiable or Satisfiable (explained in the TPTP Tech Report) like
% Status : Satisfiable
Please remove these problems from the test set: gkc will never report "satisfiable", vampire sometimes reports satisfiablility, but cannot do it in harder cases.
Also, please remove problems with the name containing the caret ^ like KRS275^7.p: these are in a typed/higher order language.
You will probably want to run Vampire like this (try also vampire --help):
vampire --mode casc --include ~/TPTP ~/TPTP/Problems/ALG/ALG150+1.p
where the --mode casc thing makes vampire try out many strategies, not just running one.
Gkc runs many strategies by default, unless you give it an extra strategy selection file as a command line arg.
The gkc method for finding included axioms (the first two are the TPTP suggestions provers mostly follow):
- try Axioms folder under the problem folder (notice you could set a sumbolic link there or just copy)
- try the TPTP environment variable, under which look for Axioms folder
- try the /opt/TPTP folder (assuming we have /opt/TPTP/Axioms/... there)
This may be helpful: an example script for provers. It is *not* exactly the script you finally need, but you may get useful inspiration/ideas.
Practice work 5
The goal of this excercise is to create a large number of search strategies and try out which ones are able to solve most problems.
For gkc either make many small strategy files or make a single large strategy file containing many runs: give each one 1 second and finally produce statistics as for which combination of strategies seems to be best for this problem class (initially experiment with KRS).
A strategy file example as given in the https://github.com/tammet/gkc top-level README:
{
"print":1,
"print_level": 15,
"max_size": 0,
"max_depth": 0,
"max_length": 0,
"max_seconds": 0,
"equality":0,
"runs":[
{"max_seconds": 1, "strategy":["negative_pref"], "query_preference": 1},
{"max_seconds": 1, "strategy":["negative_pref"], "query_preference": 0},
{"max_seconds": 1, "strategy":["query_focus"], "query_preference": 2},
{"max_seconds": 5, "strategy":["negative_pref"], "query_preference": 1},
{"max_seconds": 5, "strategy":["negative_pref"], "query_preference": 0},
{"max_seconds": 5, "strategy":["hardness_pref"], "query_preference": 0},
{"max_seconds": 5, "strategy":["unit"], "query_preference": 0}
]
}