PySAT plugin

The pysat model plugin provides the metaclases required to work with SAT models and to transform feature models into SAT.

Table of contents

  1. Description
    1. Features of the PySAT Metamodel Plugin
    2. Installation Instructions
    3. Links
  2. Operations
  3. Transformations supported

Official repository

https://www.github.com/flamapy/pysat_metamodel

Description

This plugin implements the classes to perform AAFM using the PySAT metasolver. It encompasses the set of variables and constraints objects to execute the analysis operations using PySAT as the backend. This allows us to rely on more than ten SAT solvers. This plugin offers the following functionality:

Features of the PySAT Metamodel Plugin

  1. SAT Solver Integration:
    • Integrates with the PySAT toolkit, which supports a wide range of SAT solvers.
    • Enables the framework to perform complex constraint satisfaction problems, such as checking the satisfiability of feature models and identifying dead features.
  2. Metamodel Classes:
    • Provides the necessary classes to represent the SAT-based metamodel, facilitating the transformation of feature models into SAT representations.
  3. Operations:
    • Implements various operations specific to SAT-based analysis, such as satisfiability checks, identification of core features, and detection of dead features.
    • Offers robust mechanisms for performing detailed analyses on feature models using SAT solvers.
  4. Transformations:
    • Supports Text-to-Model (T2M) transformations to read feature models and convert them into SAT representations.
    • Enables Model-to-Model (M2M) transformations to translate feature models into different formats for SAT-based analysis.
    • Facilitates Model-to-Text (M2T) transformations to serialize SAT results back into human-readable formats.

Installation Instructions

To install the pysat_metamodel plugin, follow these steps:

  1. Install Python: Ensure that Python 3.9 or later is installed on your system.

  2. Install the PySAT Metamodel Plugin:

    • Using pip, the Python package manager, you can install the flamapy-sat plugin directly from PyPI: 
      pip install flamapy-sat

Operations

Currently, this plugin enables the following operations. Note that these operations are executed without a backend solver which makes them scalable and fast while having some limitations:

Transformations supported

Currently this plugins enables a set of TextToModel transformations (a.k.a Parsers) and ModelToText transformations (a.k.a serializations) for the most common variability serializations found in the literatures. Concretely we support:

Model to text transformations

Text to model transformations

Model to model transformations