SkolemFC takes in a F(X,Y) formula as input and returns the number of Boolean functions G(X) such that ∃Y F(X, Y) = F(X, G(X)). SkolemFC counts the number of functions without even generating a single function.
To learn more about SkolemFC, please have a look at our AAAI-24 paper.
Linux:
sudo apt install build-essential cmake git libubsan1 libasan8 \
zlib1g-dev libmlpack-dev libensmallen-dev libmpfr-dev \
libboost-program-options-dev libboost-serialization-dev libgmp3-dev
macOS:
brew install cmake gmp boost mpfr mlpack
Clone the repository (including submodules) and configure:
git clone --recurse-submodules https://github.com/meelgroup/skolemfc/
cd skolemfc
./configure.sh
cd build && make -j10
Run ./configure.sh --help for the full usage message.
First, you must translate your problem to QDIMACS and just pass your file as input to SkolemFC, it will print the number of funcitons satisfying of the given QDIMACS formula.
$ ./skolemfc myfile.qdimacs
c [sklfc] SkolemFC Version: 36cf66a9ae
c [sklfc] executed with command line: ./skolemfc myfile.qdimacs
c [sklfc] using epsilon: 0.8 delta: 0.4 seed: 0
...
s fc 2 ** 4.00
...
c [sklfc] finished T: 0.25
c [sklfc] iterations: 729
SkolemFC reports that we have approximately 16 (=2 ** 4) functions satisfying the QDIMACS specification.
SkolemFC provides so-called "PAC", or Probably Approximately Correct, guarantees. In less fancy words, the system guarantees that the solution found is within a certain tolerance (called "epsilon") with a certain probability (called "delta"). The default tolerance and probability, i.e. epsilon and delta values, are set to 0.8 and 0.4, respectively. Both values are configurable.
Code in this branch does not provide theoretical guarantees. See
mainbranch for code which truly follows the paper.
Please click on "issues" at the top and create a new issue. All issues are responded to promptly.
This work is by Arijit Shaw, Brendan Juba, and Kuldeep S. Meel, as published in AAAI-24.
The benchmarks used in our evaluation can be found here.
An exact counter (termed "Baseline" in the paper) for Skolem Functions is available in the folder utils/baseline. Please follow instructions in the README inside that folder for installing tools for that.