Linux kconfig SAT integration

The Linux kernel uses kconfig to help enable configuring the kernel and try to ensure expressed dependencies are met. Kconfig has its limitations though and integrating a SAT solver is expected to help not only address some of Kconfig's limitations but also give us quite a bit advanced bells and whistles within Kconfig. This project aims at doing integration of a SAT solver into Linux by addressing the most simple use case of a SAT solver, while leaving the rest of the optional bells and whistles up for future development. For more futuristic possible uses of SAT solvers on linux refer to the linux-sat page.

At this point in time this project is simply listed as work needed, it is not associated with GSoC, Outreachy, or anything else. We are simply grouping people interested together in document why we want this, and helping mentor it getting upstream.

How you get this upstream is up to you, the developer.

Problem description

Below we'll split definitions of kconfig, SAT solvers, provide references for prior known uses of SAT solvers with Kconfig, prior stated interest in this work, then also some references to other uses of SAT Solvers used in the Linux ecosystem and finally then go into detail on evaluating proposed work of integrating a SAT solver into the Linux kernel.

More more futuristic uses of SAT solver on Linux refer to linux-sate page which documents known possible uses of SAT solvers within the Linux kernel.

Defining kconfig

Kconfig is the variability modeling languages used in Linux, used to express kernel build dependency relationships. This is done through a series of symbols and expressed relationships between symbols. A user configures a kernel build through a menu interface, the job of kconfig is to entrust the defined relationships expressed by developers and then ensure that the only sensible symbols are displayed which will not create any build or run time conflicts.

Defining a SAT solver

A SAT solver specializes in evaluating if there exists an interpretation that satisfies a given boolean formula. In the simplest case this in turn will tell you if a series of variables and their relationships are satisfiable or not. This won't explain why things are unsatisfiable though, or what is the minimal set of satisfiable set of variables that are allowed. There are advanced aspects of SAT solving though that deal with later elements of the satisfiable question, for instance a A SAT solver with Minimally Unsatisfiable Subformulas (MUSes) support should be able to show the minimum set of variables which can be enabled that are satisfiable.

Previous SAT solver kconfig integration work

In May 2010, Vegard Nossum announced a GSoC project to use a SAT solver to generate full kernel configs based on a set of constraints given by the user. As of May 2016, the project is usable in practice but not yet merged. The patchset embeds PicoSAT and includes three new targets:

The biggest missing feature is proper handling of string/int/hex options in the solver -- these values are currently derived from defaults or explicit settings.

To pull the code, do: git fetch v4.3+kconfig-sat (or see

The project is aiming for upstream inclusion once the last bugs have been sorted out.

Non-upstream SAT solver use in Linux with Kconfig

Two research projects are known to have toyed with using SAT solvers for Linux and Kconfig:

SAT solver uses in the Linux ecosystem

SAT solvers have also been used in other areas of the Linux distribution ecosystem. One of the known areas was for package dependency resolution. The 3 year Mancoosi research project challenged researchers and developers with solutions for software package resolution dependencies requiring free software licenses for proposed solutions, some of the solutions proposed used SAT solvers, one of which was CryManSolver which used CryptoMiniSat (github) as backend (a SAT solver in itself).

SAT software candidates for Linux kconfig integration

The obvious candidates currently evaluated have been:

Integrating a SAT into Linux only makes sense if we know we can count on support from SAT solving experts to help with long term maintenance and issues, we have confirmation of interest to help Linux's integration and future issues by both SAT solver experts, the authors of both PicoSAT and CryptoMiniSat - Armin Biere and Máté Soós.

SAT solver integration on kconfig upstream

This section documents why and how its envisioned we can integrate a SAT solver into Linux for use by Kconfig.

A simple desirable feature to strive for to start off with Kconfig is to have the option to avoid displaying symbols from the configurator, or make a symbol unselectable (and optionally explain then why its not selectable if selected) if its known that selecting a symbol would break an existing configuration. Kconfig will currently avoid displaying a symbol only if its dependencies explicitly annotated with a with 'depends on' cannot be met, however conflicts and implicit dependencies with 'select' are ignored. This is actually a feature of how kconfig 'select' works to help with loading a preset known set of required symbols for an architecture. Select can however be used widely on drivers and its use then can cause unexpected issues when configuring the kernel. Even if 'select' is used within architecture Kconfig files, if a symbol is being selected by architecture but it leads to possibly broken configuration state we want to know about this and fix these issues.

This is one task, let's break this task down further:

1) seems to be the crux of the work required, we have tools that do 2) but we don't want independent tools, but rather an integrated solution. One can stage work by first implementing 1) and then using an existing tool to test 2).

Optional advanced features one can strive for:

kconfig heavy handed select

Kconfig currently enables a select to be enabled without first evaluating if the symbols that the selectable has would conflict or create an issue with any of the known currently set set of symbols. This is actually a feature of kconfig, given select was designed to be heavy handed for architecture to preload a set of symbols it needs. Kconfig then currently does not check the list of symbols listed on a symbol's "select" list, this is done on purpose to help load a set of known required symbols. Because of this use of select should be used with caution.

The option B and C are clearly contradicting with respect to A. However, when A is set, C can be set as well because Kconfig does not visit the dependencies of the select target (in this case B). And since Kconfig does not visit the dependencies, it breaks the dependencies of B (!A).

This is best shown with the following sample Kconfig file. Copy

Test with:

Copy and paste the following code into a file called, note though you will need to fix tons spacing issues to use, alternatively you can just download this file which has the spacing issues addressed.

Mentors and areas of expertise

Interested developers

Folks considering hacking on this and getting this upstream:

Mailing list

We'll eventually use the mailing list for upstream development discussions, but for now we'll want you to use this specialized list:

Anyone can subscribe. Count on the above folks as being subscribed.



KernelNewbies: KernelProjects/kconfig-sat (last edited 2017-12-30 01:30:35 by localhost)