Pedant

Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) based on interpolation-based definition extraction and Counterexample-Guided Inductive Synthesis (CEGIS).

Installing PEDANT

Dependencies

• Boost
• CMake >= 3.4
• GCC

Optional Dependencies

Learning default function requires:

• mlpack

Using the validation tool requires:

• Python
• PySAT

Included Dependencies

Pedant is shipped with the following third party programs. Note that for some of these programs, Pedant uses adapted versions.

• CaDiCaL
• Glucose
• Minisat
• Aiger
• ABC
• avy
• docopt.cpp

Build

We only provide instructions for building PEDANT on a LINUX system.

git clone --recursive https://github.com/fslivovsky/pedant-solver pedant
cd pedant
mkdir build && cd build
cmake ..
make

To enable machine learning use -DUSE_ML=ON when calling cmake. If the tool for validating certificates is not needed use -DBUILD_CERT_TOOLS=OFF when calling cmake.

Usage

pedant [Options] <Input> 

where Input shall be the path to a DQDIMACS file. To get a list of options pedant --help can be used.

Input

Pedant expects the input to be given as a PCNF in DQDIMACS format. DQDIMACS extends QDIMCACS by allowing to explicitly state the dependencies of an existential variable. For this purpose DQDIMACS introduces the d quantifier block. In the following we give a simple example of a DQDIMACS file:

p cnf 4 2
a 1 2 0
d 3 1 0
d 4 2 0
1 -3 0
2 3 4 0

The above DQDIMACS represents the DQBF ∀u1 ∀u2 ∃e1(u1) ∃e2(u2) (u1 ∨ ¬e1) ∧ (u2 ∨ e1 ∨ e2).

Validation of Certificates

The subdirectory certification contains the python script certifyModel.py. This script can be used to validate certificates generated by Pedant. To run this script use:

certifyModel.py <Formula> <Certificate> 

Inputs

• Formula the DQDIMACS of interest
• Certificate a certificate that was generated by PEDANT for Formula. The certificate can be given in each of the supported formats.

Output

• 0 if certification succeeded.
• 1 if certification did not succeed.

Example

We illustrate the usage of Pedant and the validation script with the following sample DQDIMACS, which we call formula.dqdimacs.

p cnf 5 3
a 1 2 0
e 3 0
d 4 1 0
d 5 2 0
-1 4 0
2 -5 0
1 -2 3 4

To run Pedant we can use:

pedant formula.dqdimacs --aag model

Pedant will report that the formula is satisfiable and it will generate a certificate in the ASCII Aiger format. Next we can validate the generated certificate by:

certifyModel.py formula.dqdimacs model

This will print Model validated!.