Satisfiable configuration

Description: Checks if there exists at least one valid configuration that satisfies a given set of selected and deselected features.

Application: Useful for validating partial configurations and ensuring they can be completed into full valid configurations.

Example: Verifying if a partial configuration with a selected set of features can lead to a valid product without any constraint violations.

---

Code Examples

Command line usage

flamapy satisfiable_configuration "path/to/feature/model" "path/to/configuration"

Python easy to use facade usage

from flamapy.interfaces.python.flamapy_feature_model import FLAMAFeatureModel
# Load the feature model
fm = FLAMAFeatureModel("path/to/feature/model")
# Identify if it is a satisfiable configuration
operation = fm.satisfiable_configuration(("path/to/configuration"), full_configuration=False)
print(operation)

Python flamapy framework usage

from flamapy.core.discover import DiscoverMetamodels
# Initiallize the dicover metamodel
dm = DiscoverMetamodels()
# Call the operation. Transformations will be automatically executed; 
# Use BDDSatisfiableConfiguration or Z3SatisfiableConfiguration to rely on other solvers
result = dm.use_operation_from_file(operation_name="PySATSatisfiableConfiguration",
                                  file="path/to/feature/model", 
                                  configuration_file='path/to/configuration',
                                  is_full=False)
print(result)

Python flamapy framework ADVANCED usage

from flamapy.core.discover import DiscoverMetamodels
# Initiallize the dicover metamodel
dm = DiscoverMetamodels()
# Get the fm metamodel representation using the transformation 
# required to get to the fm metamodel
feature_model = dm.use_transformation_t2m("path/to/feature/model",'fm') 
# Get the configuration representation using the transformation 
# required to get to the configuration metamodel
configuration = dm.use_transformation_t2m('path/to/configuration','configuration')
# Manually call a M2M transformation to Pysat
sat_model = dm.use_transformation_m2m(feature_model,"pysat")
# Get the operation
operation = dm.get_operation(sat_model,'PySATSatisfiableConfiguration')
# Set the configuration within the operation
configuration.is_full=False
operation.set_configuration(configuration)
# Execute the operation
operation.execute(sat_model)
# Get and print the result
result = operation.get_result()
print(result)

---

Facade signature: satisfiable_configuration(self, configuration_path: str, full_configuration: bool = False, backend: Optional[str] = None, *, allow_approximate: Optional[bool] = None)

Inputs:

name	type	required	default
configuration_path	str	yes	—
full_configuration	bool	no	False

Default backend: sat (selectable via backend=)

Implemented by:

plugin	exact	scale limit
z3_metamodel	yes	—
pysat_metamodel	yes	—
bdd_metamodel	yes	1000