The iCNF file format
This document was written in 2009, and the provided patches were last updated in 2011. The webpage has been moved to its current URL www.siert.nl/icnf in November 2014.The iCNF file format is based on the DIMACS CNF format which is commonly used as input to SAT solvers, see for a sufficient description the input format requirements of the SAT competition. The problem line found in the normal DIMACS CNF format specifies the number of variables and clauses in the formula. In the iCNF format the problem line is always exactly the following:
p inccnfThe problem line is only to identify the file as an iCNF file and it contains no further information. After the problem line there are clauses in the usual format mixed with assumption lines. Each assumption line starts with an a, which is followed by a sequence of non-zero integers representing literals and terminated by a zero. A file in the iCNF format defines a sequence of formulas: Each assumption line represents the formula that is formed by the conjunction of all clauses preceding that line and all literals on that line. Note that the syntax of the assumption line is, apart from the leading a, the same as that of a clause but it represents a conjunction of literals rather than a disjunction. The iCNF file format was designed such that it is suitable for streaming an unknown length sequence of incrementally encoded formulas into a solver. This is why the number of variables and clauses are not to be specified on the problem line.
cThis example corresponds to a formula sequence containing the following two formulas:
Solving the formula sequenceA simple single threaded solver for these files starts by reading all clauses up to the first assumption line. After this it solves those clauses assuming the value true for each literal on the assumption line, and reports the result. It then continues by reading all clauses up to the second assumption line, after which it solves the whole set under the assumption that all literals in the second assumption are true, etc.
patch < minisat-2.2.0-for-icnf.patch
Generating files in the iCNF format
Note added in 2014: The remainder of this document is probably no longer interesting to any potential iCNF users.If this patch is applied to NuSMV 2.4.3 it is extended with two extra commands gen_ltlspec_sbmc_inc and pipe_ltlspec_sbmc_inc. The first command allows the generation of an iCNF file from an SMV model and an LTL property. The second allows NuSMV to pipe an iCNF file into an external application while it is being generated on-the-fly. The patch includes modification for various NuSMV source files and can be applied to all those files at once by copying it into NuSMV's nusmv/src directory and executing in that directory the following command:
patch -p1 < nusmv-2.4.3-for-icnf.patchIt is not necessary to link an external SAT solver to NuSMV to make the iCNF generating functions work.
Example usageAssuming that you have downloaded the patch for NuSMV 2.4.3, applied it and compiled the resulting code you could enter the following sequence of commands after executing the resulting binary:
read_model -i example.smv
If you have an SMV model in a file example.smv which includes a single LTL property specified in an LTLSPEC line the result is a file example.icnf. This file is in the iCNF format and describes a sequence of 36 incremental SAT problems (corresponding to counterexample lenghts 0..35).
We can now solve the sequence in example.icnf using for example the modified version of MiniSAT obtained using the patch found above. Assuming that the binary for that modified MiniSAT version is named /my_patched_minisat/minisat on your system you could have also entered the following into NuSMV:
read_model -i example.smv
Which would make NuSMV execute /my_patched_minisat/minisat and pipe the iCNF output into its standard input. This allows solving parts of the sequence before the complete sequence is generated. Anything that proceeds the -s parameter is assumed to be part of the shell command to be executed, so -s must be the last of the parameters meant for the pipe_ltlspec_sbmc_inc command itself. For example:
pipe_ltlspec_sbmc_inc -k 35 -s /my_patched_minisat/minisat -verbosity=2 -polarity-mode=trueWould execute MiniSAT with the specified verbosity and polarity-mode parameters.
The pipe_ltlspec_sbmc_inc terminates whenever the executed shell command terminates, even if the problem has not been generated up to the requested depth. This is useful as for example the patched MiniSAT version includes a command line option stopatsat which will make it terminate whenever it finds SAT, which might be at a much smaller bound than the one up to which NuSMV attempts to generate the encoding. Note that the result of piping into the patched MiniSAT version is thus essentially the same as executing the check_ltlspec_sbmc_inc command with the original MiniSAT solver linked to NuSMV. It does however offer much greater flexibility as any program that accepts the iCNF format can be used. The obvious downside is that the satisfying assignment that may be found is not communicated back into NuSMV and can thus not be pretty printed as an execution of the SMV model.