Component-oriented optimization of SAT encodings

Despite once being described as a “killer app” by Donald Knuth due to its versatility, SAT is far from being utilized to its full potential. One area where this has become especially apparent is variant configuration, a field known for its lack of standardization and high proportion of proprietary models. Despite the wide variety of approaches for variability modeling systems, there is little public research on the efficiency and optimization potential of symbolic-logic based solutions. This work is based on DMalizer, a framework that analyzes the linear variability models of an industry partner and transforms them into non-linear configurators based on SMT. This SMT encoding allows for improvements in the configuration workflow but struggles with performance, prompting the creation of our novel encoding using SAT. By combining our domain-specific knowledge and the low-level approach of SAT, we implement different variants for components within the SAT formula and evaluate their performance in metrics such as speed and scalability. We use the results of our benchmarks to determine which variants show the greatest optimization potential for our SAT-based configurators, as well as how different parameters within the variability model influence these results.