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 forFormula
. 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!
.