uvl2dimacs: Optimized translation from universal variability language into Boolean logic

This is the authors' abstract. We don't add key points for this paper.

The Universal Variability Language (UVL) serves as the primary standard for describing variability models in configurable software systems. SAT/#SAT technology and knowledge-compilation tools, which are commonly used for configuration checking, feature analysis, product counting, and generating uniform random samples, require input in the DIMACS format. This paper presents uvl2dimacs , a C++ tool that converts UVL specifications into DIMACS by providing two complementary techniques: a Tseitin transformation, which limits exponential clause growth, and backbone simplification, which shortens and eliminates clauses by identifying fixed literals. An evaluation of 1,533 real-world models from the UVLHub public repository demonstrates the tool’s correctness and effectiveness. Backbone simplification reduces the number of clauses in 99.09% of models (with a median reduction of 40.43%), while the Tseitin transformation achieves clause reduction in only 0.65% of models (but with a median reduction of 83.11% in those cases).