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

[  news | download | license | background ]

CNF2AIG

News

This converter extracts an AIG in AIGER format from a CNF in DIMACS format.

First public release. This is still beta software.

Download

[ cnf2aig-1.tar.gz ]

License

In essence we use a BSD style licences for CNF2AIG. Please refer to the LICENSE file for more details.

Background

CNF is a popular input format for SAT solvers. However, it lacks information about the structure of the formula respectively circuit. This information can be useful to speed up SAT solving. See for instance the recent paper by Eén, Mishchenko, and Sörensson, presented at SAT'07. Therefore it can be useful to extract a structural representation out of of a flat CNF. The tool has also been used to generate some benchmarks for the AIG track of the SAT'07 SAT Solver competition.