Solver Demo

We demonstrate and benchmark the functionality of multiple SAT/SMT/MIP solvers/optimizers in multiple programming languages. This repo serves as a playground for various research projects.

Use cases include:

Use case	File(s)/folder(s)	Related project repo	Related paper
Counting (by enumerating) all solutions for a simple AND or OR formula	c_solvers/*, java_solvers/*, python_solvers/Solver_Enumeration_Benchmark.ipynb	repo	paper
MIP/SMT models of a simple knapsack problem	java_solvers/ChocoOptimizationDemo.java, python_solvers/Knapsack_Demo.ipynb, python_solvers/Z3_Demo.ipynb	repo	paper
SMT model of finding alternative subgroup descriptions	python_solvers/alternative_subgroup_description_demo.py	repo	arxiv
MIP model (and greedy algorithm) of decision tree for selecting algorithm configurations	python_solvers/configuration_selection_tree_demo.py
MIP/SMT models of different filter feature-selection techniques	python_solvers/filter_fs_benchmark.py	repo	arXiv, journal
MIP/SMT models of multi-task feature selection inspired by solver portfolios	python_solvers/fs_portfolio_demo.py
SMT model of discovering functional dependencies	python_solvers/functional_dependency_demo.py
MIP models of different set-cover problems	python_solvers/set_cover_demo.py
MIP/SMT models of the (simultaneous) alternative-feature-selection problem	python_solvers/simultaneous_afs_benchmark.py	repo	arXiv, journal
MIP/SMT models of the k-portfolio problem	python_solvers/small_portfolios_demo.py	repo	paper
SMT model of a simultaneous multi-round auction	python_solvers/SMR_Auction_Demo.ipynb	repo	paper
MIP/SMT models of the subgroup-discovery problem	python_solvers/subgroup_discovery_demo.py	repo	arxiv

Testing Solvers for Constrained Feature Selection

Solver	Languages	Hints
Choco	Java	also an optimizer
Gecode	C++	also an optimizer
GEKKO	Python	mainly an optimizer
Google OR Tools	Java, Python	also an optimizer
PicoSAT	Python
pySMT	Python	wraps various solvers (e.g., MathSAT, Z3)
python-constraint	Python
Z3	C++, Java, Python	also an optimizer

For all three languages (C++, Java, Python), we also implement own solution counters/enumerators:

• option 1 ("arithmetic enumeration"): tailored to the specific benchmark formulas (AND, OR), converted to an arithmetic representation
• option 2 ("flexible enumeration"): for arbitrary logical expressions, constructed in an object-oriented manner

Setup

Python Code

The code resides in directory python_solvers/. We use Python 3.8.3 (in particular, out of Anaconda3 2019.10) with conda 4.8.3 dependency management. For reproducibility purposes, we exported our environment with conda env export --no-builds > environment.yml. You should be able to import the environment via conda env create -f environment.yml and then activate it with conda activate solver-demo. After activating, call ipython kernel install --user --name=solver-demo to make the environment available for notebooks.

Java Code

The code resides in directory java_solvers/. We use Java 8. For the Java code, you can import java_solvers as a Maven project into Eclipse.

ArithmeticEnumerationDemo and FlexibleEnumerationDemo don't have any external dependencies.

ChocoDemo and ChocoOptimizationDemo should also work directly, as their dependency is hosted on Maven Central.

For Z3Demo, matters are more complicated. First, please download a pre-built version of Z3 and extract it. (If that's too easy for you, you can also try to compile it.) Our project also has a Maven dependency on Z3, but the Z3 download only provides a plain JAR. Thus, extract Maven somewhere on your computer and add it to your PATH (optional). Next, install the Z3 JAR into your local Maven repository (might need to adapt file path and version):

mvn install:install-file -Dfile=com.microsoft.z3.jar -DgroupId=com.microsoft -DartifactId=z3 -Dversion=4.8.7 -Dpackaging=jar

Furthermore, the JAR depends on DLLs also included in the Z3 download. To enable access, add the bin/ directory of your Z3 download to the environment variable Path.

For ORToolsDemo, the process is similar, download is here , but you need to build two Maven artifacts.

C++ Code

The code resides in directory c_solvers/.

arithmetic_enumeration_demo and both flexible_enumeration_demos don't have any external dependencies.

For z3_demo, you need the pre-built version of Z3, as for the Java pendant. You can put the C++ file in a Visual Studio project. Make sure to adapt (for all configurations, all platforms):

• Project -> Properties -> Configuration Properties -> C/C++ -> General -> Additional Include Directories by adding the path to the include/ directory of the Z3 download.
• Project -> Properties -> Configuration Properties -> Linker -> General -> Additional Library Directories by adding the path to the bin/ directory of the Z3 download.
• Project -> Properties -> Configuration Properties -> Linker -> Input -> Additional Dependencies by adding libz3.lib.

For gecode_demo, you also need to install or compile the software and reference the DLLs in a similar manner. See the documentation for more details.