SAT solver for LINUX

Potential supervisors: 
Research groups/keywords: 
Description: 

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: http://kernelnewbies.org/KernelProjects/kconfig-sat

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