Algoritmide ja andmestruktuuride erikursus

Course name: Advanced Algorithms and Data Structures in Automated Reasoning

Course code: ITI8590 Semester: fall 2019 Lecturer: Tanel Tammet Contact: tanel.tammet@ttu.ee, 6203457, ICT 426 Language: The default language of the course is English, but if all students understand Estonian, it will be in Estonian. Lectures per week: 1 lecture, 2 academic hours Practice work per week: 1 session, 2 academic hours Home work: additionally, mostly development and experimentation

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}
    ]
 }