Improving Linux kernel configuration using a boolean satisfiability constraint (SAT) solver

by Vegard Nossum for Portland State University

The main idea of my project is to integrate a proper boolean satisfiability constraint (SAT) solver into the kernel configuration system. The SAT solver takes as input a list of boolean variables and constraints (formulae which must be true) for these variables, and finds assignments for the variables such that the constraints are satisfied. Using a SAT solver would greatly improve the usability and safety of the kernel's configuration system.