fix: count reliably via UniGen's ApproxMC and drop pyapproxmc

The standalone pyapproxmc binding mis-configures ApproxMC's projected counting on
feature-model CNFs with implied variables (the root and mandatory-relation unit
clauses), undercounting by a factor of two (e.g. 408 instead of 816). UniGen's
ApproxMC invocation does not have that problem, so obtain the count through
pyunigen (num=0, projected onto the feature variables) and drop the pyapproxmc
dependency entirely — pyunigen bundles ApproxMC and covers both counting and
sampling. Add a regression test for models with implied variables.

Author: José Ángel Galindo Duarte

README.md

@@ -19,7 +19,7 @@ It complements the existing backends:
 pip install flamapy-sharpsat
 ```
 
-This pulls in `pyapproxmc` and `pyunigen` (and the flamapy core/FM/SAT plugins).
+This pulls in `pyunigen` (which bundles ApproxMC), and the flamapy core/FM/SAT plugins.
 
 ## Operations
 

flamapy/metamodels/sharpsat_metamodel/operations/sharpsat_configurations_number.py

@@ -1,6 +1,6 @@
 from typing import cast
 
-import pyapproxmc
+import pyunigen
 
 from flamapy.core.models import VariabilityModel
 from flamapy.core.operations import ConfigurationsNumber
@@ -13,6 +13,12 @@ class SharpSATConfigurationsNumber(ConfigurationsNumber):
     Counting is projected onto the feature variables, so auxiliary variables (e.g. Tseytin
     gates) do not inflate the result. ApproxMC gives an (epsilon, delta) probabilistic
     approximation that scales far better than exact enumeration.
+
+    The count is obtained through UniGen's binding (``pyunigen`` with ``num=0``, which runs
+    ApproxMC's projected count without drawing samples). The standalone ``pyapproxmc`` binding
+    mis-configures ApproxMC's projected counting on feature-model CNFs with implied variables
+    (the root and mandatory-relation unit clauses), undercounting by a factor of two; UniGen's
+    ApproxMC invocation does not have that problem.
     """
 
     def __init__(self, seed: int = 1) -> None:
@@ -27,9 +33,11 @@ def get_result(self) -> int:
 
     def execute(self, model: VariabilityModel) -> 'SharpSATConfigurationsNumber':
         sharpsat_model = cast(SharpSATModel, model)
-        counter = pyapproxmc.Counter(seed=self._seed)
+        counter = pyunigen.Sampler(seed=self._seed)
         for clause in sharpsat_model.clauses:
             counter.add_clause(clause)
-        cell_count, hash_count = counter.count(sharpsat_model.feature_variables())
+        cell_count, hash_count, _samples = counter.sample(
+            num=0, sampling_set=sharpsat_model.feature_variables()
+        )
         self._result = cell_count * (2 ** hash_count)
         return self

pyproject.toml

@@ -14,7 +14,6 @@ dependencies = [
     "flamapy-fw~=2.6.0.dev4",
     "flamapy-fm~=2.6.0.dev4",
     "flamapy-sat~=2.6.0.dev4",
-    "pyapproxmc~=4.3",
     "pyunigen~=2.5",
 ]
 

tests/test_sharpsat.py

@@ -60,6 +60,31 @@ def _is_valid(fm: FeatureModel, selected: set) -> bool:
     return op.execute(sat_model).get_result()
 
 
+_IMPLIED_VARS_UVL = """features
+    Root {abstract}
+        mandatory
+            Base
+                mandatory
+                    Core
+        optional
+            A
+            B
+            C
+constraints
+    A => B
+"""
+
+
+def _fm_from(uvl):
+    handle, path = tempfile.mkstemp(suffix='.uvl')
+    try:
+        with os.fdopen(handle, 'w') as file:
+            file.write(uvl)
+        return UVLReader(path).transform()
+    finally:
+        os.remove(path)
+
+
 def test_approximate_count_matches_exact_on_small_model():
     fm = _fm()
     exact = PySATConfigurationsNumber().execute(FmToPysat(fm).transform()).get_result()
@@ -68,6 +93,16 @@ def test_approximate_count_matches_exact_on_small_model():
     assert approx == exact
 
 
+def test_count_is_correct_with_implied_variables():
+    # Regression guard: models with implied variables (mandatory chains, root unit clause)
+    # must not be undercounted. The standalone pyapproxmc binding halved these; the UniGen
+    # ApproxMC invocation used by the counter does not.
+    fm = _fm_from(_IMPLIED_VARS_UVL)
+    exact = PySATConfigurationsNumber().execute(FmToPysat(fm).transform()).get_result()
+    approx = SharpSATConfigurationsNumber().execute(FmToSharpSAT(fm).transform()).get_result()
+    assert approx == exact
+
+
 def test_sampling_returns_valid_configurations():
     fm = _fm()
     model = FmToSharpSAT(fm).transform()