Here is a list of possible subjects for the course projects. If you have other ideas, feel free to discuss them with lecturers.
The goal here is to improve the SAT-solver that you started writing in TD1 with
This mathematical theory only says that, given a function symbol
f of unknown interpretation,
It is well-known that satisfiability problems for that theory can be solved by an algorithm called congruence closure.
Here, the project will explore how such problems can be solved in a more general context, called MCSAT,
which organises an interaction between solvers for different theories.
This is the logic that rejects the idea of reasoning by contradiction, and which is widely used in Interactive Theorem Proving.
However, there exist algorithms that can prove theorem of intuitionistic logic automatically, if they are in the propositional fragment.
The best-performing algorithm for doing this uses a very unconventional approach, described in a LPAR'2015 paper.
Two projects can be done regarding that algorithm:
First, compare it with earlier work, which it seems connected to: analyse the differences, and what could be the reason for a fundamental speed-up in the new approach.
Second, try to integrate that algorithm to a rather systematic approach for satisfiability-solving that is based on model constructing algorithms.
Most algorithms for automated reasoning have a learning mechanism that allows them to learn new facts from old facts. The database of learnt facts is very useful, because what is learnt at some point can be re-used, to speed-up the reasoning mechanisms in the future. However, the database has a tendency to grow large, and despite clever techniques to scan it efficiently, its size increase eventually becomes problematic as too much CPU time is spent searching the database, and going over useless facts, or facts that are redundant with each other. State-of-the-art provers implement clever heuristics for pruning the database every now and then, removing the most useless facts, so as to keep the database size under control. The project consists in surveying these techniques, and implement them in a prover that does not yet have this feature.
This theory has a sibling, Linear Rational Arithmetic (LRA), that is easier to automate. Universal statements in LRA can be proved or disproved by the use of (SAT-solving and) a simplex algorithm. For example, trying to prove that for all rationals x and y, either (2y < -2x + 1) or (2y > 2x + 1) or (2x > 1) is going to fail, because an obvious counter-example is x=y=1/2. However this would be provable if x and y were integers. Making sure that the counter-examples are actually integers, and not simply rationals, requires some extra work to be done on top of the simplex algorithm. Dejan Jovanovic invented for linear arithmetic a method that is rather different from the simplex algorithm, and we have implemented it for LRA. On the basis of his paper for LIA, the project would explore whether the adaptation from LRA to LIA is easier to do in his approach than in the simplex approach, and, if so, it would involve adapting our LRA implementation into an LIA implementation.
Formally verifying a neural net is asking the question of whether there is an input that can give a particular output (for instance if the neural net is used as a classifier, the question is whether there exists an input that gets mis-classified). We concentrate here on neural nets whose activation function is a max with 0. Technically, answering such a question for a given neural net requires solving linear arithmetic problem with case analyses for each max. Nothing theoretically difficult, but in practice the number of cases makes the question really difficult to answer. At CAV'2017, Guy Katz presented a clever technique to explore this huge search space efficiently. The question here is whether Dejan Jovanovic's model-constructing approach (or our own variant) can be used to express or capture this clever technique, or propose something similarly efficient.
Vectors of bits are what our computers manipulate at the lowest level. Establishing that hardware or software actually operate in the way we intend them to, often requires proving properties about bitvectors. The theory of bit vectors is not theoretically difficult, but usually, the properties we want to prove involve so many bits that proving them automatically is very long. At SMT'2017, Dejan Jovanovic and I proposed a novel approach for automatically proving these properties, trying to avoid going down to the bit-level as much as possible. Part of this proposal involves BDD (Binary Decision Diagrams). The project would involve turning these vague ideas into an actual implementation (warning: this is not just implementing something completely specified; it also involves quite a bit of design).