Advanced Techniques for Grounding and Solving in the IDP Knowledge Base System
The area of Knowledge Representation and Reasoning, a subfield of Artificial Intelligence, studies how knowledge can be represented and how it can be used for automated reasoning.
Several declarative programming paradigms implement this by developing a formal language to symbolically represent knowledge, as well as an associated form of inference to achieve the desired solution.
Recently, the Knowledge Base System (KBS) paradigm has been proposed, based on the idea that knowledge is not inherently linked to a specific reasoning task.
Instead, this paradigm proposes to express knowledge in a truly declarative manner.
Additionally, to stress reusability of this knowledge, the KBS paradigm allows the knowledge to be combined with one out of a set of possible inferences, each providing a solution to some type of computational task.
The initial implementation of this KBS paradigm, also known as the IDP3 system, provided a suitable laboratory to examine a new type of software engineering.
State-of-the-art declarative programming systems such as IDP3, clasp, WASP, and lp2sat work using the ground-and-solve methodology.
First, the high-level language is ground into a low-level propositional language.
As a second step the grounding is used as input for general-purpose, low-level propositional (generally SAT-like) solvers.
This thesis contains a thorough study of the impact of different grounding approaches on the solver behaviour.
I.e., if the grounding process that is used is smart and results in a smaller low-level representation, does this impact the search behaviour of the underlying solver?
The language supported by the IDP3 system contains constraints and definitions.
For the purpose of this thesis, we split up definitions into two kinds: input* (also called intentional or stratified predicates, or domain atoms) and search definitions.
Input* definitions are definitions that depend on concepts that are known beforehand and can be evaluated.
One contribution of this thesis is the evaluation of input* definitions using Tabled Prolog.
In order to use these techniques, definitions have to be transformed into a format usable by Prolog.
The main challenge in this transformation is correctly projecting away the types and rich language constructs, whilst taking into acount Prolog's left-to-right execution mechanism.
Search definitions on the other hand cannot be evaluated because they depend on unknown data.
This text elaborates how the above translation to Prolog can be re-used: 1) to partially evaluate definitions, deriving as much information as possible, and 2) ground definitions using a Tabled Prolog execution mechanism.
We developed a method to guide the solver to focus on relevant parts in the search space.
Only the part of the specification that is linked with the current search branch of the problem has to be taken into account.
The goal of this technique is to prevent certain decisions from being made once it is possible to prove that they will not influence the outcome of searching in the current search branch.
Additionally, this leads us to an improved stopping criterion for SAT(ID) solvers since any state without relevant decisions is considered an end state, instead of only states in which all literals have been decided.
An implementation of technique is presented.
The implementation uses a incremental approach, adjusting certain data structures based on the changes in the solver state.
With this work we intend to increase the usability of the IDP3 system and elevate it to a "mature" Knowledge Base System.