qbf4j

QBF is an immutable data structure, representing quantified boolean formula trees containing the following connectives:

• ¬ - negation
• ∧ - conjunction
• ∨ - disjunction
• ∀ - universal quantification
• ∃ - existential quantification

Features

• Java 8 Stream support
• structural pattern matching using QBF::accept and QBF::apply (Church encoding)
• reading/writing of QCIR-G14 and QDIAMCS files
• transformation into
  • cleansed form
  • negation normal form
  • prenex normal form
  • conjunctive normal form

Prerequisites

• Ant >= 1.9
• Java >= 1.8

Installation

Build from source using ant dist and include dist/qbf4j-VERSION.jar in the classpath.

Executables

qcir2pnf

Converts a given QCIR-G14 formula into prenex normal form.

> $ java -jar dist/qcir2pnf-VERSION.jar

Usage: qcir2pnf [OPTION]... <input-file> <output-file>

  -s <class>, --strategy=<class>  prenexing strategy to apply, where <class>
                                  is the fully qualified name of a class
                                  implementing the PrenexingStrategy interface,
                                  e.g.:

                                  at.jku.fmv.qbf.pnf.ExistsDownForAllUp
                                  at.jku.fmv.qbf.pnf.ExistsUpForAllDown
                                  at.jku.fmv.qbf.pnf.ForAllDownExistsDown
                                  at.jku.fmv.qbf.pnf.ForAllDownExistsUp
                                  at.jku.fmv.qbf.pnf.ForAllUpExistsDown
                                  at.jku.fmv.qbf.pnf.ForAllUpExistsUp (default)

  -c [<class>], --cnf[=<class>]   transform to PCNF, where <class> is the fully
                                  qualified name of a class implementing the
                                  CNFEncoder interface, e.g.:

                                  at.jku.fmv.qbf.pcnf.PG86 (default)

  --cleanse                       cleanse formula

  --qdimacs                       output formula in QDIMACS format

Benchmarks

qbf4j contains benchmarks for critical functions using JMH.

After building the benchmarks using ant benchmark, see java -jar dist/qbf4j-VERSION-benchmark.jar -h for available command line options.

Listing all available benchmarks is done using:

java -jar dist/qbf4j-VERSION-benchmark.jar -l

For running a preconfigured version of a specific benchmark, use:

java -cp dist/qbf4j-VERSION-benchmark.jar <class>.<method>

To show an overview of a benchmark's result in markdown format, a simple python script is included at:

src/benchmark/python/printBenchmark.py

Tree Size

To measure the formula tree size of the given test set run:

java -cp dist/qbf4j-VERSION-benchmark.jar -javaagent:dist/qbf4j-VERSION-QBFSizeAgent.jar QBF.MemoryConsumption

Test Sets

Any *.qcir or *.qdimacs file can be used for running benchmarks.

The following bash scripts may be used to download and extract a test set:

• qcir non-prenex test set (archive) default
• qbfeval'17 test set (archive)

Configuration

A properties file for customizing certain benchmark parameters can be found at:

src/benchmark/resources/benchmark.properties

After changing the properties file, either run ant benchmark to rebuild the jar file or include it in the classpath when running a benchmark.