STP constraint solver

Simple Theorem Prover SMT solver

Cnf Output Format

This page describes the output format that STP uses when passed the --output-cnf option. For example:

1
2
3
4
5
6
7
8
9
10
c Result of efficient AIG-to-CNF conversion using package CNF
p cnf 7 8
2 3 -4 6 0
2 4 -5 6 0
2 -4 5 6 0
-2 -6 0
-2 4 5 0
-2 -3 -4 -5 0
7 0
2 0

Lines beginning with c are comment lines, which are disregarded.

The line beginning with p is the problem line, which is of the format p cnf nvars nclauses where nvars and nclauses are the number of variables and clauses, respectively.

Each other line encodes one clause. Clauses are defined as a list of literals followed by a 0. Positive literals are 1, 2, …, and negative literals are -1, -2, ….

The code that generates the output file is in extlib-abc/aig/cnf/cnfMan.c.