Manthan takes in a F(X,Y) formula as input and returns Boolean function \Psi such that \exists Y F(X, Y) = F(X,\Psi(X)). Manthan works at the intersection of machine learning, constrained sampling, and automated reasoning.
To read more about Manthan, have a look at CAV-20 paper and ICCAD-21 paper. You can also refer to the related slides and the talk video.
- Python 3+
To install the required libraries, run:
python -m pip install -r requirements.txt
Manthan depends on:
- Open-WBO and RC2 for MaxSAT queries
- PicoSAT to compute unsat core.
- Scikit-Learn to create decision trees to learn candidates.
- ABC to represent and manipulate Boolean functions.
- UNIQUE to extract the unique functions.
Manthan employ the algorithmic routine proposed by BFSS to do preprocessing. We used a CryptoMiniSAT based framework to do the preprocessing.
In the dependencies directory, you will find 64-bit x86 Linux compiled binaries for the required dependencies.
To install Unique: Make sure you have python-sat installed.
git clone https://github.com/perebor/unique.git
cd unique
git checkout 1902a5aa9573722cf473c7e8b5f49dedf9a4646d
git submodule init
git submodule update
mkdir build
cd build
cmake .. && make
Now, clone Manthan
git clone https://github.com/meelgroup/manthan
cd manthan
ln -s ../unique/build/interpolatingsolver/src/itp.cpython-38-x86_64-linux-gnu.so itp.so
Note: the exact file name of the .so file in the last line may vary, depending on your version of Python.
python manthan.py <qdimacs input> A simple invocation with benchmarks/max64.qdimacs
python manthan.py benchmarks/max64.qdimacs
starting Manthan
parsing
count X variables 128
count Y variables 290
preprocessing: finding unates (constant functions)
count of positive unates 7
count of negative unates 5
finding uniquely defined functions
count of uniquely defined variables 277
parsing and converting to verilog
generating weighted samples
generated samples.. learning candidate functions
generated candidate functions for all variables.
verification check UNSAT
no more repair needed
number of repairs needed to converge 0
you can also provide different option to consider for manthan:
python manthan.py [options] <inputfile qdimacs>
To see detailed list of available option:
python manthan.py --help
Few benchmarks are given in benchmarks directory.
Full list of benchmarks used for our experiments is available here. The dataset includes qdimacs and verilog benchmarks.
Please click on "issues" at the top and create a new issue. All issues are responded to promptly.
@inproceedings{GRM20,
author={Golia, Priyanka and Roy, Subhajit and Meel, Kuldeep S.},
title={Manthan: A Data-Driven Approach for Boolean Function Synthesis},
booktitle={Proceedings of International Conference on Computer-Aided Verification (CAV)},
month={7},
year={2020}
}
@inproceedings{GSRM21,
author={Golia, Priyanka and Slivovsky, Friedrich and Roy, Subhajit and Meel, Kuldeep S.},
title={Engineering an Efficient Boolean Functional Synthesis Engine},
booktitle={Proceedings of International Conference On Computer Aided Design (ICCAD)},
month={7},
year={2021}
}
- Priyanka Golia ([email protected])
- Subhajit Roy ([email protected])
- Kuldeep Meel ([email protected])