Gorde:
| Egile Nagusiak: | , , , |
|---|---|
| Formatua: | Recurso digital |
| Hizkuntza: | |
| Argitaratua: |
Zenodo
2026
|
| Sarrera elektronikoa: | https://doi.org/10.5281/zenodo.19682330 |
| Etiketak: |
Etiketa erantsi
Etiketarik gabe, Izan zaitez lehena erregistro honi etiketa jartzen!
|
Aurkibidea:
- <div class="markdown-heading"> <h1 class="heading-element">UVL2Dimacs</h1> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#uvl2dimacs"></a></div> <p>A C++ library and CLI tool for converting Universal Variability Language (UVL) feature models to DIMACS CNF format.</p> <p><a href="https://github.com/rheradio/uvl2dimacs/blob/main"></a> <a href="https://github.com/rheradio/uvl2dimacs/blob/main"></a> <a href="https://github.com/rheradio/uvl2dimacs/blob/main/LICENSE"></a></p> <div class="markdown-heading"> <h2 class="heading-element">Table of Contents</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#table-of-contents"></a></div> <ul> <li><a href="https://github.com/rheradio/uvl2dimacs#features">Features</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#requirements">Requirements</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#build">Build</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#basic-usage">Basic Usage</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#cli-options">CLI Options</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#api-usage">API Usage</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#conversion-modes">Conversion Modes</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#backbone-simplification">Backbone Simplification</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#testing">Testing</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#uvl-grammar-support">UVL Grammar Support</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#output-format">Output Format</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#performance">Performance</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#api-documentation">API Documentation</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#project-structure">Project Structure</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#limitations">Limitations</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#authors">Authors</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#license">License</a></li> <li><a href="https://github.com/rheradio/uvl2dimacs#related-tools">Related Tools</a></li> </ul> <div class="markdown-heading"> <h2 class="heading-element">Features</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#features"></a></div> <ul> <li><strong>Two Conversion Modes</strong>: <ul> <li><strong>Straightforward</strong> (direct CNF, fewer variables, compact)</li> <li><strong>Tseitin</strong> (auxiliary variables for cross-tree constraints, preventing exponential clause growth)</li> </ul> </li> <li><strong>Backbone Simplification</strong>: 30-50% formula size reduction while preserving solution counts</li> <li><strong>High Performance</strong>: Optimized with -O3, LTO, and native CPU tuning</li> <li><strong>Library API</strong>: Clean C++ API for integration into other tools</li> <li><strong>Comprehensive Testing</strong>: 1,533 test models with automated solution count verification</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">Requirements</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#requirements"></a></div> <ul> <li>C++17 compiler (g++ or clang++)</li> <li>CMake 3.10+</li> <li>GNU Make</li> <li>zlib development headers (required by MiniSat)</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">Build</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#build"></a></div> <div class="markdown-heading"> <h3 class="heading-element">1. Install a C++ Compiler</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#1-install-a-c-compiler"></a></div> <p><strong>Linux (Ubuntu/Debian):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo apt-get update <span class="pl-k">&&</span> sudo apt-get install g++</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Linux (Fedora/RHEL):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo dnf install gcc-c++</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>macOS:</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>xcode-select --install</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h3 class="heading-element">2. Install zlib Development Headers</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#2-install-zlib-development-headers"></a></div> <p>zlib is required by MiniSat (the SAT solver embedded in the backbone simplifier).</p> <p><strong>Linux (Ubuntu/Debian):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo apt-get update <span class="pl-k">&&</span> sudo apt-get install zlib1g-dev</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Linux (Fedora/RHEL):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo dnf install zlib-devel</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>macOS:</strong> zlib is bundled with Xcode Command Line Tools — no separate install needed.</p> <div class="markdown-heading"> <h3 class="heading-element">3. Install CMake</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#3-install-cmake"></a></div> <p><strong>Linux (Ubuntu/Debian):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo apt-get update <span class="pl-k">&&</span> sudo apt-get install cmake</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Linux (Fedora/RHEL):</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>sudo dnf install cmake</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>macOS:</strong></p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>brew install cmake</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h3 class="heading-element">4. Compile</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#4-compile"></a></div> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre><span class="pl-c"># Build everything</span> make <span class="pl-c"># Build specific targets</span> make uvl2dimacs <span class="pl-c"># CLI tool</span> make api <span class="pl-c"># API library</span> make examples <span class="pl-c"># API examples</span></pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">Basic Usage</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#basic-usage"></a></div> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre><span class="pl-c"># Convert UVL to DIMACS</span> ./build/uvl2dimacs input.uvl output.dimacs <span class="pl-c"># With backbone simplification (reduces formula size)</span> ./build/uvl2dimacs -b input.uvl output.dimacs <span class="pl-c"># Tseitin transformation</span> ./build/uvl2dimacs -t input.uvl output.dimacs</pre> <div class="zeroclipboard-container"> </div> </div> <p>1,533 ready-to-use UVL models are available in <code>tests/straightforward/uvl/</code> and can be used directly as inputs. For example:</p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>./build/uvl2dimacs tests/straightforward/uvl/automotive01.uvl output.dimacs</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">CLI Options</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#cli-options"></a></div> <div class="snippet-clipboard-content notranslate position-relative overflow-auto"> <pre class="notranslate"><code>Usage: uvl2dimacs [-t|-s] [-b] <input.uvl> <output.dimacs> Options: -s Use straightforward conversion (default) -t Use Tseitin transformation with auxiliary variables -b Apply backbone simplification to reduce formula size Examples: uvl2dimacs model.uvl output.dimacs # Basic conversion uvl2dimacs -b model.uvl output.dimacs # With backbone uvl2dimacs -t -b model.uvl output.dimacs # Tseitin + backbone </code></pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">API Usage</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#api-usage"></a></div> <div class="markdown-heading"> <h3 class="heading-element">Basic Conversion</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#basic-conversion"></a></div> <div class="highlight highlight-source-c++ notranslate position-relative overflow-auto"> <pre>#<span class="pl-k">include</span> <span class="pl-s"><span class="pl-pds"><</span>uvl2dimacs/UVL2Dimacs.hh<span class="pl-pds">></span></span> uvl2dimacs::UVL2Dimacs converter; <span class="pl-k">auto</span> result = converter.convert(<span class="pl-s"><span class="pl-pds">"</span>model.uvl<span class="pl-pds">"</span></span>, <span class="pl-s"><span class="pl-pds">"</span>output.dimacs<span class="pl-pds">"</span></span>); <span class="pl-k">if</span> (result.success) { std::cout << <span class="pl-s"><span class="pl-pds">"</span>Features: <span class="pl-pds">"</span></span> << result.<span class="pl-smi">num_features</span> << std::endl; std::cout << <span class="pl-s"><span class="pl-pds">"</span>Variables: <span class="pl-pds">"</span></span> << result.<span class="pl-smi">num_variables</span> << std::endl; std::cout << <span class="pl-s"><span class="pl-pds">"</span>Clauses: <span class="pl-pds">"</span></span> << result.<span class="pl-smi">num_clauses</span> << std::endl; }</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h3 class="heading-element">Tseitin Mode</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#tseitin-mode"></a></div> <div class="highlight highlight-source-c++ notranslate position-relative overflow-auto"> <pre>uvl2dimacs::UVL2Dimacs converter; converter.set_mode(uvl2dimacs::ConversionMode::TSEITIN); <span class="pl-k">auto</span> result = converter.convert(<span class="pl-s"><span class="pl-pds">"</span>model.uvl<span class="pl-pds">"</span></span>, <span class="pl-s"><span class="pl-pds">"</span>output.dimacs<span class="pl-pds">"</span></span>); <span class="pl-k">int</span> aux_variables = result.num_variables - result.num_features; std::cout << <span class="pl-s"><span class="pl-pds">"</span>Auxiliary variables: <span class="pl-pds">"</span></span> << aux_variables << std::endl;</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h3 class="heading-element">With Backbone Simplification</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#with-backbone-simplification"></a></div> <div class="highlight highlight-source-c++ notranslate position-relative overflow-auto"> <pre>uvl2dimacs::UVL2Dimacs converter; converter.set_mode(uvl2dimacs::ConversionMode::STRAIGHTFORWARD); converter.set_backbone_simplification(<span class="pl-c1">true</span>); converter.set_verbose(<span class="pl-c1">true</span>); <span class="pl-k">auto</span> result = converter.convert(<span class="pl-s"><span class="pl-pds">"</span>model.uvl<span class="pl-pds">"</span></span>, <span class="pl-s"><span class="pl-pds">"</span>output.dimacs<span class="pl-pds">"</span></span>);</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h3 class="heading-element">Complete Examples</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#complete-examples"></a></div> <p>See <a href="https://github.com/rheradio/uvl2dimacs/blob/main/api/examples"><code>api/examples/</code></a> for detailed usage:</p> <ul> <li><a href="https://github.com/rheradio/uvl2dimacs/blob/main/api/examples/simple_convert.cc"><code>simple_convert.cc</code></a> - Basic conversion with both modes and backbone simplification</li> <li><a href="https://github.com/rheradio/uvl2dimacs/blob/main/api/examples/tseitin_convert.cc"><code>tseitin_convert.cc</code></a> - Dedicated Tseitin example</li> <li><a href="https://github.com/rheradio/uvl2dimacs/blob/main/api/examples/batch_convert.cc"><code>batch_convert.cc</code></a> - Batch processing with mode comparison and performance metrics</li> <li><a href="https://github.com/rheradio/uvl2dimacs/blob/main/api/examples/backbone_convert.cc"><code>backbone_convert.cc</code></a> - Converts a model with and without backbone simplification and prints a side-by-side reduction summary</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">Conversion Modes</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#conversion-modes"></a></div> <p>UVL2Dimacs supports two CNF transformation strategies, each optimized for different use cases.</p> <div class="markdown-heading"> <h3 class="heading-element">Straightforward Mode (Default, <code>-s</code>)</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#straightforward-mode-default--s"></a></div> <p>Direct CNF conversion with 1 variable per feature.</p> <ul> <li>Fewer variables, compact representation</li> <li>Best for most models</li> <li>May produce longer clauses for complex constraints</li> </ul> <p><strong>When to use</strong>: General-purpose feature models, when minimizing variable count is important, and models with simple Boolean constraints.</p> <div class="markdown-heading"> <h3 class="heading-element">Tseitin Mode (<code>-t</code>)</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#tseitin-mode--t"></a></div> <p>Auxiliary variables for cross-tree constraint expressions; feature tree relations are emitted directly.</p> <ul> <li>Prevents exponential clause growth in nested Boolean cross-tree constraints</li> <li>Fewer auxiliary variables (only introduced where needed)</li> <li>Feature tree relation clauses (OR groups, ALTERNATIVE groups, cardinality) emitted directly as CNF</li> </ul> <p><strong>When to use</strong>: Models with deeply nested Boolean cross-tree constraint expressions.</p> <div class="markdown-heading"> <h3 class="heading-element">Comparison</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#comparison"></a></div> <table> <tbody><tr> <th>Aspect</th> <th>Straightforward</th> <th>Tseitin</th> </tr> </tbody><tbody> <tr> <td><strong>Variables</strong></td> <td>Fewer (n features)</td> <td>More (n + auxiliaries for cross-tree constraints)</td> </tr> <tr> <td><strong>Feature tree relation clauses</strong></td> <td>Direct (arbitrary length)</td> <td>Direct (arbitrary length)</td> </tr> <tr> <td><strong>Cross-tree constraint clauses</strong></td> <td>May grow exponentially</td> <td>Linear size</td> </tr> <tr> <td><strong>Best for</strong></td> <td>General use</td> <td>Deeply nested cross-tree constraints</td> </tr> </tbody> </table> <p><strong>Both modes preserve solution counts</strong> (verified by test suite).</p> <p>See <a href="https://github.com/rheradio/uvl2dimacs/blob/main/docs/translation.md">docs/translation.md</a> for detailed transformation rules, Tseitin encoding, and comprehensive examples.</p> <div class="markdown-heading"> <h2 class="heading-element">Backbone Simplification</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#backbone-simplification"></a></div> <p>Optional optimization that reduces CNF formula size by 30-50% while preserving solution counts.</p> <p><strong>Quick example:</strong></p> <ul> <li>Input: 17 variables, 39 clauses</li> <li>Output: 17 variables, 18 clauses (54% reduction)</li> <li>Solution count: Preserved (verified)</li> </ul> <p><strong>Works with both modes</strong> (straightforward and Tseitin).</p> <p>See <a href="https://github.com/rheradio/uvl2dimacs/blob/main/docs/translation.md#backbone-simplification">docs/translation.md § Backbone Simplification</a> for algorithm details, proof of correctness, performance characteristics, and feature model applications (core/dead feature detection).</p> <div class="markdown-heading"> <h2 class="heading-element">Testing</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#testing"></a></div> <p>UVL2Dimacs includes comprehensive verification suites with <strong>1,533 real-world UVL models</strong> from <a href="https://www.uvlhub.io/" rel="nofollow">uvlhub.io</a>.</p> <div class="markdown-heading"> <h3 class="heading-element">Test Model Collection</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#test-model-collection"></a></div> <p><strong>Location</strong>: <code>uvl2dimacs/tests/straightforward/</code> contains 1,533 pure Boolean UVL models</p> <p><strong>Coverage</strong>:</p> <ul> <li>Model sizes: 4 to 500+ features</li> <li>Relation types: MANDATORY, OPTIONAL, OR, ALTERNATIVE, CARDINALITY</li> <li>Real-world domains: automotive, software product lines, embedded systems</li> </ul> <div class="markdown-heading"> <h3 class="heading-element">Straightforward Conversion Verification</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#straightforward-conversion-verification"></a></div> <p>Verifies that the straightforward converter produces the expected DIMACS output:</p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>bash tests/straightforward/test_straightforward.sh</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Method</strong>: Runs <code>uvl2dimacs -s</code> on all 1,533 UVL models and compares generated DIMACS files against reference files, ignoring comment lines.</p> <p><strong>Expected</strong>: All tests PASS with identical CNF content.</p> <div class="markdown-heading"> <h3 class="heading-element">Prerequisites for Solution-Counting Tests</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#prerequisites-for-solution-counting-tests"></a></div> <p>The Backbone and Tseitin test suites internally use <a href="https://github.com/Laakeri/sharpsat-td">SharpSAT-TD</a> for exact #SAT counting.</p> <p><strong>Install GMP, MPFR, and CMake:</strong></p> <ul> <li>Ubuntu/Debian: <code>sudo apt-get install libgmp-dev libmpfr-dev cmake</code></li> <li>Fedora/RHEL: <code>sudo dnf install gmp-devel mpfr-devel cmake</code></li> <li>macOS: <code>brew install gmp mpfr cmake</code></li> </ul> <p><strong>Note</strong>: The backbone test scripts automatically build SharpSAT-TD from source for the current platform and provide OS-specific installation instructions if dependencies are missing.</p> <div class="markdown-heading"> <h3 class="heading-element">Backbone Simplification Verification</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#backbone-simplification-verification"></a></div> <p>Verifies that backbone simplification preserves exact solution counts:</p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre><span class="pl-c"># Test 20 models (default)</span> bash tests/backbone/test_backbone.sh <span class="pl-c"># Test more models</span> bash tests/backbone/test_backbone.sh 50</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Method</strong>: Generates DIMACS with/without backbone, counts solutions with SharpSAT-TD, verifies equality.</p> <p><strong>Expected</strong>: All tests PASS with identical solution counts.</p> <blockquote> <p><strong>Note</strong>: This script automatically builds SharpSAT-TD from source into <code>tests/sharpsat-td/</code>. <strong>Run the backbone test before the Tseitin test</strong> — the Tseitin test expects the binary to already be present.</p> </blockquote> <div class="markdown-heading"> <h3 class="heading-element">Tseitin Transformation Verification</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#tseitin-transformation-verification"></a></div> <p>Verifies that the Tseitin transformation preserves exact solution counts.</p> <blockquote> <p><strong>Prerequisite</strong>: Run <code>bash tests/backbone/test_backbone.sh</code> first to build SharpSAT-TD.</p> </blockquote> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre><span class="pl-c"># Test 20 models (default)</span> bash tests/tseitin/test_tseitin.sh <span class="pl-c"># Test specific number</span> bash tests/tseitin/test_tseitin.sh 100</pre> <div class="zeroclipboard-container"> </div> </div> <p><strong>Method</strong>: Generates DIMACS in both straightforward and Tseitin modes, counts solutions, and verifies equality.</p> <p><strong>Expected</strong>: All tests PASS with identical counts, confirming full biconditional equivalences (⟺).</p> <div class="markdown-heading"> <h2 class="heading-element">UVL Grammar Support</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#uvl-grammar-support"></a></div> <div class="markdown-heading"> <h3 class="heading-element">Feature Types</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#feature-types"></a></div> <ul> <li><strong>Mandatory</strong>: Child must be selected if parent is selected</li> <li><strong>Optional</strong>: Child may be selected when parent is selected</li> </ul> <div class="markdown-heading"> <h3 class="heading-element">Group Types</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#group-types"></a></div> <ul> <li><strong>Or</strong>: At least one child must be selected</li> <li><strong>Alternative</strong>: Exactly one child must be selected</li> <li><strong>Cardinality [n..m]</strong>: Between n and m children must be selected</li> </ul> <div class="markdown-heading"> <h3 class="heading-element">Constraints</h3> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#constraints"></a></div> <ul> <li>Boolean operators: <code>&</code> (AND), <code>|</code> (OR), <code>!</code> (NOT)</li> <li>Implications: <code>=></code> (IMPLIES), <code><=></code> (IFF)</li> <li>Shortcuts: <code>requires</code>, <code>excludes</code></li> </ul> <p><strong>Example UVL Model:</strong></p> <div class="snippet-clipboard-content notranslate position-relative overflow-auto"> <pre class="notranslate"><code>features Car mandatory Engine optional GPS alternative Gasoline Electric constraints Electric => GPS </code></pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">Output Format</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#output-format"></a></div> <p>DIMACS CNF format with feature mappings:</p> <div class="snippet-clipboard-content notranslate position-relative overflow-auto"> <pre class="notranslate"><code>c Generated by UVL2Dimacs c Feature mapping: c 1 Car c 2 Engine c 3 GPS c 4 Gasoline c 5 Electric p cnf 5 8 1 0 -1 2 0 -2 1 0 -1 4 5 0 -4 -5 0 -4 1 0 -5 1 0 -5 3 0 </code></pre> <div class="zeroclipboard-container"> </div> </div> <p>Each clause is a space-separated list of literals (positive/negative integers) terminated by <code>0</code>.</p> <div class="markdown-heading"> <h2 class="heading-element">Performance</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#performance"></a></div> <p>The build uses aggressive optimization:</p> <ul> <li><code>-O3</code> (maximum optimization)</li> <li><code>-march=native -mtune=native</code> (CPU-specific tuning)</li> <li><code>-flto</code> (link-time optimization)</li> <li><code>CMAKE_INTERPROCEDURAL_OPTIMIZATION=ON</code></li> </ul> <p><strong>Typical performance:</strong></p> <ul> <li>Small models (<100 features): <10ms</li> <li>Medium models (100-500 features): 10-100ms</li> <li>Large models (500+ features): 100-1000ms</li> <li>Backbone simplification adds 50-200ms depending on model size</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">API Documentation</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#api-documentation"></a></div> <p>Generate full API documentation with Doxygen:</p> <div class="highlight highlight-source-shell notranslate position-relative overflow-auto"> <pre>make docs open docs/html/index.html</pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">Project Structure</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#project-structure"></a></div> <div class="snippet-clipboard-content notranslate position-relative overflow-auto"> <pre class="notranslate"><code>uvl2dimacs/ ├── api/ # High-level API │ ├── include/ # Public API headers │ ├── src/ # API implementation │ └── examples/ # Usage examples ├── cli/ # Command-line interface ├── generator/ # Core CNF generation │ ├── include/ # Feature model and CNF classes │ └── src/ # Transformation implementation ├── parser/ # ANTLR-generated UVL parser │ ├── include/ # Parser/lexer headers │ └── src/ # Generated ANTLR4 source files ├── backbone_solver/ # Backbone computation tool │ ├── bin/ # Compiled backbone_solver binary │ ├── docs/ # Backbone algorithm documentation │ └── src/ # Source (api, cli, data_structures, detectors, io, minisat, minisat_interface) ├── tests/ # Test suites │ ├── sharpsat-td/ # Model counter (shared) │ ├── backbone/ # Backbone verification tests │ ├── tseitin/ # Tseitin verification tests (includes dimacs/ reference files) │ └── straightforward/ # 1,533 test models (UVL + DIMACS) ├── antlr/ # ANTLR4 C++ runtime ├── docs/ # Documentation └── build/ # Build output </code></pre> <div class="zeroclipboard-container"> </div> </div> <div class="markdown-heading"> <h2 class="heading-element">Limitations</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#limitations"></a></div> <ul> <li><strong>Boolean feature models only</strong>: Arithmetic and comparison operators in cross-tree constraints are silently skipped (they require SMT, not pure SAT).</li> <li><strong>Feature cardinality not expanded</strong>: The UVL <code>cardinality [n..m]</code> annotation on individual features (indicating multi-instance features) is parsed but not processed; only group cardinality is supported.</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">Authors</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#authors"></a></div> <ul> <li>Rubén Heradio (<a href="mailto:rheradio@issi.uned.es">rheradio@issi.uned.es</a>)</li> <li>David Fernández Amorós (<a href="mailto:david@issi.uned.es">david@issi.uned.es</a>)</li> <li>Ismael Abad Cardiel (<a href="mailto:iabad@issi.uned.es">iabad@issi.uned.es</a>)</li> <li>Ernesto Aranda-Escolástico (<a href="mailto:earandae@issi.uned.es">earandae@issi.uned.es</a>)</li> </ul> <div class="markdown-heading"> <h2 class="heading-element">License</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#license"></a></div> <p>MIT License - see <a href="https://github.com/rheradio/uvl2dimacs/blob/main/LICENSE">LICENSE</a> file for details</p> <div class="markdown-heading"> <h2 class="heading-element">Related Tools</h2> <a class="anchor" href="https://github.com/rheradio/uvl2dimacs#related-tools"></a></div> <ul> <li><a href="https://www.uvlhub.io/" rel="nofollow">UVL Hub</a> - Repository of UVL feature models</li> <li><a href="https://universal-variability-language.github.io/" rel="nofollow">UVL Specification</a> - Official UVL documentation</li> <li><a href="https://github.com/Laakeri/sharpsat-td">SharpSAT-TD</a> - Tree decomposition-based #SAT solver</li> </ul> <p><strong>UVL2Dimacs</strong> - Bridging feature modeling and SAT solving.</p>