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.

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.

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.)