Algorithm selection for model counting
as4moco uses algorithm selection and automated algorithm configuration decrease its solving time for #SAT queries. It is based on AutoFolio, an algorithm selection framework.
- Java 21
- Python 3 (tested for Python 3.10)
- Ubuntu 22.04 (other version may require a recompilation of the used solver binaries)
- Install modified AutoFolio
- Create a new virtual environment:
python3 -m venv <Name of Virtual Environment>
- Clone modified AutoFolio:
git clone https://github.com/RSD6170/AutoFolio/
- Install the modified AutoFolio package:
<path to venv>/bin/python3 -m pip install <path to cloned repository>
- Create a new virtual environment:
- Clone this repository:
git clone https://github.com/SoftVarE-Group/as4moco
- Modify AlgorithmSelector.java at marked todo with path to python venv and AutoFolio repository:
private final static String[] commands = new String[]{"<Path to Python Venv>/bin/python3", "-u", "<Path to AutoFolio repo>/scripts/java_bridge.py"};
Run Gradle::run
with your parameters
Example for Ubuntu: ./gradlew run −−args="−modelFile </path/to/af_model.pkl> −cnfFile </path/to/cnf.dimacs>"
New model files can be created, refer to the example in the AutoFolio repository.