UG Projects 2019-2020

Dr. Hana Chockler

I am offering the following UG projects in 2019-20 academic year. Each project can be done as a third year UG or fourth year MSci project.

The topics are related to my research interests and are based on my expertise.

Please note that the projects contain a theoretical and a practical part (implementation). You will be required to submit your source code as a part of the project report, and to include a demo of your implementation in your final project presentation.

In 2019-20, the supervision of projects is done in groups. Therefore, the projects are offered as topics with a number of variations. Each student will work on a variant of the topic, defined by the supervisor. The project meetings will be organised around common topics.

[HC01] Writing a SAT solver

The problem of finding a satisfying assignment for a given Boolean formula is known as SAT problem and it is a hard problem in general. However, there are many tools that solve SAT and in practice they work well in the majority of cases. These tools can be roughly divided into those that follow the DPLL algorithm and those that rely on stochastic methods. The tools employ heuristics to find satisfying assignments (such as backtracking, conflict resolution, etc.). These heuristics are tuned to a particular type of instances, and hence are expected to perform well on those instances (and possibly be significantly worse than others on a different type of instances).

In this project, the student will write a small SAT solver and evaluate it on a number of instances.

We will hold a SAT Solver competition at the time of project presentations, modelled after the official annual SAT competition. The competition is in BYOB format (Bring Your Own Benchmark), hence all benchmarks are expected to be in the same format. We will use DIMACS format, which is also the format used in the official SAT competition.

Variants of the DPLL-based SAT solver:

Tuned to randomly generated balanced instances (that is, each variable appears without negation roughly the same number of times as with negation).
Tuned to randomly generated imbalanced instances (that is, variables appear significantly more frequently in one of the polarities - can be different for each variable).
Tuned to efficient solving of instances derived from graph colouring problems.
Tuned for efficient solving of unsatisfiable instances.

Variants of the Stochastic SAT solver:

Stochastic SAT solver based on genetic algorithms.
Stochastic SAT solver based on simulated annealing and optimisations, but not genetic algorithms.

Skills needed for the project:

Good programming skills in a language of your choice (preferably Java, for performance).
Some understanding of algorithms and the ability to apply the theoretical knowledge to implementation.

[HC02] Suggest your own project.

This includes both the returning year in industry students, who would like to continue working with their placement company and are able to identify an isolated development project as their final UG project, and students who would like to propose their own project as a final UG project. The project's scope and structure should be consistent with the requirements for the final UG or MSci project. If you have an idea that you would like to pursue as your final project, please come to talk to me, and I can help you to define it as a suitable project if possible.

Please note that the projects supervised by me should have a theoretical and a practical component.