Below are several ideas that can form the starting point for a student research project that I would be happy (and capable) to supervise. These ideas all have a reasonably concrete research question as starting point, and they are (likely) feasible to carry out.

These projects are suitable for, for example, an small research project or a thesis project (in the context of the MSc Logic or the MSc Artificial Intelligence at the UvA).

Please get in touch with me (Ronald de Haan) if you are interested in any of these projects, or if you have questions about any of them.

 

1. Developing a reasoning algorithm for BSML

Bilateral state-based modal logic (BSML) is a modal logic that has been used, for example, in recent work by colleagues on pragmatics.

I have built a (rough) prototype for a reasoning algorithm for BSML that is based on answer set programming. This prototype can reason about small formulas in a reasonable amount of time. In terms of how well this algorithm (and variants of it) scales to larger formulas, much remains to be explored.

There are a lot of directions for improving this reasoner, and many of them are very much suitable for a small research project or a thesis. For some suggestions for research directions, see the demonstration of the prototype.

  • The project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • The project also requires a basic understanding of modal logic.
  • The project is algorithmic in nature, and involves some programming in Python.

 

2. Testing a declarative method to specify CEGAR-algorithms

Counterexample-guided Abstraction Refinement (CEGAR) algorithms often provide a productive method for solving problems at higher levels of the Polynomial Hierarchy (PH). In the context of SAT solving or answer set solving (for problems at the second level of the PH), this type of algorithm typically looks as follows. One solver is given an encoding of candidate solutions to the problem (the abstraction), and it starts the search process and iterates over candidate solutions. There is a second solver that is running, which is given an encoding that expresses what counterexamples for candidate solutions should satisfy. Each candidate solution produced by the first solver is given to the second solver, in the form of assumptions. If the second solver does not find a counterexample, the candidate solution is returned as an actual solution. If the second solver does find a counterexample, this counterexample is used to produce a new constraint (a refinement) that is added to the first solver, and the first solver's search process continues.

The encodings given to the first and second solver in this architecture are typically specified declaratively, using propositional logic or logic programs. The way in which refinements are produced from counterexamples are mostly given in a procedural way—e.g., in the form of a subalgorithm that produces a constraint from a counterexample. If these refinements were also specified declaratively—e.g., by just stating the properties that define them—the entire algorithm specification could be more readable and easier to modify.

This research project involves studying to what extent solving search problems at the second level of the PH by declaratively specified CEGAR-style algorithms leads to more readable (and more easily adaptable) encodings, while not giving up too much in terms of algorithmic efficiency.

There is a prototype system available, based on answer set programming, that can be used as a starting point.

  • This project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • The project is algorithmic in nature, and involves some programming in Python.

 

3. Arbitrary propositional formulas under answer set semantics

Disjunctive answer set programming (dASP) is expressive enough to model search problems at the second level of the Polynomial Hierarchy (PH). Intuitively, these problems can be expressed using an "∃∀"-quantified statement. However, expressing such problems in dASP typically leads to unnatural (and unreadable) encodings.

Answer set (or stable model) semantics has also been defined for arbitrary (propositional) logic formulas—instead of just for disjunctive logic programs, that can be seen as conjunctions of implications of a particular form. In terms of expressive power and succinctness, disjunctive logic programs and general propositional formulas are equivalent under answer set semantics.

This research project involves studying to what extent expressing natural search problems at the second level of the PH using general propositional formulas (under answer set semantics) leads to easier-to-understand and more natural encodings.

Optionally, the project can also include developing (ASP-based) algorithms for general propositional formulas under answer set semantics, and studying whether problems can be solved (more) efficiently using the developed problem encodings.

  • This project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • This project also requires a basic understanding of computational complexity theory. Students that have taken the course Computational Complexity at the UvA are well prepared for this.
  • This project is mostly theoretical in nature, and affinity with logic is recommended.
  • This project can also have an algorithmic aspect, which would involve some programming in Python.

 

4. What is needed for a productive completeness theory?

Most settings in which the theory of computational complexity has been used share certain elements. Think, for example, of the framework of NP-completeness. There is a domain of problems (in the example, NP problems), among which there are some efficiently solvable problems, for some notion of efficiency (e.g., the P problems). There is a notion of reductions between problems that is transitive and such that the efficiently solvable problems are closed under these reductions (e.g., polynomial-time many-one reductions). Moreover, the reductions are not so strong that everything in the entire domain is reducable to the efficiently solvable problems (e.g., not everything is trivially reducible to a P problem). There is also typically a natural and useful problem that is complete under the notion of reductions for the entire domain of problems (e.g., SAT is NP-complete). The working hypothesis is that the entire domain of problems is not efficiently solvable (e.g., P &neq; NP), from which it follows that complete problems are not efficiently solvable.

The following are examples of frameworks where these elements appear (naming only the domain; the efficiently solvable problems; the notion of reduction; and a natural complete problem):

  • NP, P, polynomial-time Turing reductions, SAT;
  • NP, P, logspace many-one reductions, SAT;
  • NL, L, logspace many-one reductions, graph reachability;
  • PSPACE, P, polynomial-time many-one reductions, TQBF;
  • nucomp-NP, comp-P, nucomp-reductions, ε-SAT—see, e.g., Cadoli, Donini, Liberatore, Schaerf (2002);
  • computably enumerable sets, computable sets, m-reductions, the diagonal Halting probem;
  • PLS, FP, PLS-reductions, Max-Cut/Flip;
  • EPT, SUBEPT, serf-reductions, k-SAT;
  • #P, FP, poly-time parsimonious reductions, #SAT;
  • Learning problems (where solutions can be evaluated efficiently), PAC-learnable problems, PAC-reductions, learning 3DNF formulas;
  • W[1], FPT, fpt-reductions, k-Clique;
  • Chopped-W[1], fpt-comp-FPT, fpt-comp-reductions, Clique-Completion—see, e.g., Arteche (2022);

Most (but not all) of these settings are remarkably effective, in the sense that they provide a way of classifying for nearly all problems that fit the setting whether or not they fall in the efficiently problems (under the assumption that not all problems in the domain are efficiently solvable, i.e., by showing that the problems are either efficiently solvable or complete for the domain). It is not a priori clear why these frameworks should be so effective.

Moreover, some of these frameworks lead to a multitude of complete problems, whereas other frameworks only have very few (carefully phrased) complete problems.

The aim of this project is to provide a starting point for getting a theoretical handle on why these frameworks are so effective, and why some frameworks give more (natural) complete problems than others. The main method for providing such a starting point is to develop a general, high-level, conceptual meta-framework in which all these frameworks can be expressed, and in which one can investigate the similarities and differences between these frameworks.

  • This project requires a solid understanding of computational complexity theory. Students that have taken the course Computational Complexity at the UvA are well prepared for this.
  • This project is mostly theoretical in nature, and affinity with logic is recommended.

 

5. Extending an educational game to practice logic programming

Answer set programming (ASP) is a form of declarative, logic programming, which is typically not intuitive for students that have mostly experience with imperative programming. To facilitate learning logic programming languages (such as ASP), I have developed a prototype educational game (that is inspired by General Game Playing).

This game is played on a grid, where the player can control one or more elements (that can typically move around on the grid). A scenario in the game consists of (1) a description of the rules of the game (i.e., what moves are allowed under what conditions, and what are the effects of moves), (2) a description of the goals of the game (i.e., when is the game won by the player), (3) a description of what part of the game board is visible to the player, and (4) a description of how levels are (randomly) generated. The player has to specify (5) a strategy for what moves to make, that can only use observable information. All these descriptions as well as the strategy are (to be) specified using Answer Set Programming, using a dedicated signature for specifying moves, etc.

This research project involves developing further scenarios for this game (and possibly extending the game itself), that ideally provide students a wide range of engaging and fun opportunities to learn a diverse set of logic programming skills. The main challenge in this project is to think of engaging scenarios that align with various learning goals. An additional dimension of difficulty lies in the implementation of these scenarios (in answer set programming).

  • This project requires a solid understanding of answer set programming. Students that have taken the course Knowledge Representation and Reasoning at the UvA are well prepared for this.
  • The project is algorithmic in nature, and involves some programming in Javascript and Answer Set Programming.