Finding compact representations of pseudo-Boolean polynomials is important for efficient reasoning in verification and optimization. This thesis/project studies how to represent integer pseudo-Boolean polynomials using flipped variables in order to obtain the shortest equivalent formulation.

The goal of this project is to implement and combine existing simplifications in Vampire to handle AC (associative-commutative) symbols efficiently, or devise new approaches.

This project involves the following possible topics in the area of string solving:

• investigating reduction or simplification rules for extended string operations,
• optimisation of regex (including simplifying regex in general or skipping redundant cases in terms of regex membership constraints solving),
• algorithmic improvements of the string/Nielsen datastructures (efficiently detecting unit propagation cases, tracking integer lengths, variable substitution, etc.)

NapSAT is a research SAT solver designed to support multiple backtracking strategies. This project aims at implementing missing state-of-the-art techniques to make NapSAT more competitive and analyze their impact on backtracking variants. We are searching for a master student familiar with C++ and eager to learn sharp and precise algorithms and adapt them in a medium size solver.

Circuit verification is a key bottleneck in modern hardware design. This project/thesis explores how machine learning can support automated reasoning techniques used in verification, e.g., by guiding solvers or improving reasoning over circuit constraints.