Linux SAT integration
SAT solver technology has been advancing steadily over the last few years. A lot of these advancements can be explained by a series of competitions held in different areas which have not only spurred interest into the field but also concrete solutions. The state of the art of SAT solvers is now even shifting into hardware space, but yet remains part of ongoing research.
This page is intended to document areas of interest where a SAT solver could potentially be used on Linux, both in software or perhaps in the future with hardware assisted SAT solving solutions.
Kconfig
The first taste of a SAT solver in Linux the kernel could be with integration and use of Kconfig. The interest and work for that is being documented separately on the [http://kernelnewbies.org/KernelProjects/kconfig-sat kconfig-sat] project page.
Linux scheduler
One are could be in select_idle_sibling() where the schedular checks if the overall compute and NUMA accesses of the system would be improved if the source tasks were migrated to another target CPU. Such use would require a resolution in the thousands of CPU cycles time frame, and the size of the problems will vary depending on the number of CPUs, topology, and workloads.
In addition workload parameters in particular can vary extremely fast, its not even certain yet if these problems can be represented as a SAT problem at the moment.
Another optimization consideration would be the requirement for scheduling decisions to have all data locally avaiable, offloading such problems would very likely not be viable solution, for instance, so fully hardware assisted SAT solvers may be required.
Review of state of the art on hardware assisted SAT solvers
Hardware assisted SAT solutions are known to exist but R&D for it is still in early stages:
