SAT solver for LINUX

Potential supervisors: 
Research groups/keywords: 

This project involves integrating the Picosat SAT-solver into the Linux kernel configurator (xconfig)

Currently, there's a big interest by Linux kernel maintainers to actually incorporate a SAT solver for improving the configurator to support kernel-configuration processes (e.g., detect dead features, control visibility of option subtrees, maybe even resolve configuration conflicts). More information is available on this website:

Requirements on students:
- familiarity with C programming (the Linux kernel maintainers prefer a C-based SAT solver for easy integration; that's why they'd like to go for PicoSAT)
- familiarity with propositional logics and SAT problems
- familiarity with term rewriting (e.g., for converting the formula to CNF) would be an advantage