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.
To build on Linux, you will need the following:
sudo apt install build-essential cmake git zlib1g-dev libboost-program-options-dev libboost-serialization-dev libgmp3-dev
Now clone this repository and run ./install.sh, this should compile SkolemFC and all its dependencies.
git clone https://github.com/meelgroup/skolemfc/
cd skolemfc
./install.sh
Please follow INSTALL.md if the script reports some error, or you need more instructions for compiling in other OS, etc.
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.
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.