JKU

TNF / INF

team
contact
software
publications
teaching
jobs


GI-Dissertation Award 2020

FMCAD'20 Student Forum Best Student Contribution

SAT'20 Best Presentation Award

GCAI'19 Post and Interaction Award

IJCAI-JAIR 2019 Award

SAT'19 Best Student Paper

CAV'18 Award

HVC'17 Best Paper

ETAPS'17 Test of Time Award

HVC'15 Award

FMCAD'17 Best Paper

CADE'17 Best Paper

BMC

Handbook of Satisfiability

UML@Classroom

UML@Classroom

www.digitaltechnik.org

[  download | compile | usage ]

Automated Reencoding Software

This page provides access to software used in our HVC'12 paper.
This software can re-encode a CNF formula using a techniques called Bounded Variable Addition. Furthermore, we provide the software that is required to reproduce the results of the paper.

Download

[ bva.tar.gz ]

[  lingeling-limami2-aa61f7a-110831.tar.gz  ]

A CNF formula in DIMACS format can be given to the bva tool, which then applied the SimpleBoundedVariableAddition algorithm presented in our HVC'12 paper. The lingeling version we used for the experiments is also given above.

Compile

To compile bva run make.

Usage

The following command will perform BVA on a CNF formula FILE, and will write the rewritten formula to bva.cnf:

./formula -method=BVA2 -s -print=1 -file= FILE > bva.cnf

The paper discusses several options that have been added to the algorithm. Some of them can be specified on the command line:

-s ... do not print the result of solving the formula
-simplify=X ... X=1,run unit propagation on the formula and removes duplicate clauses. X=0, do not perform simplification
-complement=X ... X=1, prefer the complement, if it is found. X=0, pick the literal with the maximum occurence
-limit=X ... run BVA until the limit is reached