SSAT Solver: Stochastic Boolean Satisfiability Solver

Introduction

This is a C++ implemantation of the algorithms proposed in Solving Stochastic Boolean Satisfiability under Random-Exist Quantification and Solving Exist-Random Quantified Stochastic Boolean Satisfiability via Clause Selection to solve random-exist SSAT (RE-SSAT) and exist-random SSAT (ER-SSAT) formulas, respectively.

Installation

Type make to complie and the executable is bin/abc

make

It has been tested successfully under CentOS 7.3.1611 with GCC_VERSION=4.8.5

Execution

Run ./bin/abc from your console and execute command ssat to solve both RE-SSAT and ER-SSAT formulas. ssat -h shows detailed arguments of the command. You can also run the ssat command from the console, as the following examples show.

RE-SSAT

./bin/abc -c "ssat ./expSsat/ssatRE/random/3CNF/sdimacs/rand-3-40-120-20.165.sdimacs"

ER-SSAT

./bin/abc -c "ssat ./expSsat/ssatER/planning/ToiletA/sdimacs/toilet_a_02_01.2.sdimacs"

Benchmarks

All benchmarks are in directory expSsat/. There are two formats (sdimacs and ssat) for RE-SSAT and three formats (sdimacs, ssat, and maxcount) for ER-SSAT. A brief description for each file format and benchmark family is as follows.

Format

sdimacs

The input file format for the implementation in this repository. It adapts the qdimacs format for quantified Boolean formulas and encodes a randomly quantified (with probability p) variable x as r p x 0. For example, the SSAT query exist x1, exist x2, random p=0.5 x3, random p=0.5 x4. (x1 or x3) and (x2 != x4). is encoded as follows.

p cnf 4 3
e 1 0
e 2 0
r 0.5 3 0
r 0.5 4 0
1 3 0
2 4 0
-2 -4 0

ssat

The input file format for the software implementing the algorithm proposed in "DC-SSAT: A Divide-and-conquer Approach to Solving Stochastic Satisfiability Problems Efficiently" by Stephen M. Majercik and Byron Boots. The SSAT query mentioned above is encoded as follows.

4
3
1 x1 E
2 x2 E
3 x3 R 0.5
4 x4 R 0.5
1 3 0
2 4 0
-2 -4 0

maxcount

The input file format for the software implementing the algorithm proposed in "Maximum Model Counting" by Daniel J. Fremont, Markus N. Rabe, and Sanjit A. Seshia. The SSAT query mentioned above can be converted to a maximum model counting query and encoded as follows.

c max 1 0
c max 2 0
c ind 3 0
c ind 4 0
p cnf 4 3
1 3 0
2 4 0
-2 -4 0

Family

RE-SSAT (in directory ssatRE)

1. random: Randomly generated k-CNF formulas with a prefix where a half of variables are randomly quantified with probability 0.5, followed by the other half existentially quantified.
2. PEC: SSAT formulas encoding the probabilistic equivalence checking problem proposed in "Towards Formal Evaluation and Verification of Probabilistic Design" by Nian-Ze Lee and Jie-Hong R. Jiang.
3. stracomp: SSAT formulas generated by changing the universal quantifers to random quantifiers of the QBFs encoding the strategic company problem proposed in "Default Logic as a Query Language" by M. Cadoli, T. Eiter, and G. Gottlob.

ER-SSAT (in directory ssatER)

1. random: Randomly generated k-CNF formulas with a prefix where a half of variables are existentially quantified, followed by the other half randomly quantified with probability 0.5.
2. MPEC: SSAT formulas encoding the maximum probabilistic equivalence checking problem proposed in "Towards Formal Evaluation and Verification of Probabilistic Design" by Nian-Ze Lee and Jie-Hong R. Jiang.
3. planning: SSAT formulas generated by changing the universal quantifers to random quantifiers of the QBFs encoding various planning problems in QBFLIB.
4. MaxCount: SSAT formulas generated by converting the benchmarks used in "Maximum Model Counting" by Daniel J. Fremont, Markus N. Rabe, and Sanjit A. Seshia.