Pedant is a solver for Dependency Quantified Boolean Formulas (DQBF) based on interpolation-based definition extraction and Counterexample-Guided Inductive Synthesis (CEGIS).
Learning default function requires:
Using the validation tool requires:
Pedant is shipped with the following third party programs. Note that for some of these programs, Pedant uses adapted versions.
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.
pedant [Options] <Input>
where Input
shall be the path to a DQDIMACS file.
To get a list of options pedant --help
can be used.
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)
.
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>
Formula
the DQDIMACS of interestCertificate
a certificate that was generated by PEDANT for Formula
. The certificate can be given in each of the supported formats.0
if certification succeeded.1
if certification did not succeed.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!
.