/cse/faculty/avg/Sat/ResProof/fileformat.txt
VERSION 1.2 Jan 10, 2005.
AUTHOR Allen Van Gelder, avg where? at cs.ucsc.edu
COPYRIGHT Allen Van Gelder, May, 2004. All rights reserved. Permission is
granted to reproduce this document for noncommercial research purposes.
1. SPECIFICATION FOR RESOLUTION PROOF FILES (PROPOSED)
---------------------------------------------------
The file format for a resolution proof is the following, where
bytes are numbered from 0, and double quotes indicate character sequences
that are NOT null-terminated:
0-3 "%RES"
4-7 format specs, terminated by white space.
The following formats will definitely be accepted:
"L32 " denotes little-endian 32-bit (e.g., Intel);
e.g., 258 is written as 02 01 00 00 hex.
"B32 " denotes big-endian 32-bit (e.g., Sparc, MIPS);
e.g., 258 is written as 00 00 01 02 hex.
"A32 " denotes ASCII signed integers separated by white
space; e.g. use printf format "%ld\n".
The remaining formats are for future development:
"L64 " denotes little-endian 64-bit (e.g., Intel);
"B64 " denotes big-endian 64-bit (e.g., Sparc, MIPS);
"A64 " denotes ASCII signed 64-bit integers.
8-31 two unsigned ASCII integers, n and m, representing the
number of variables and number of clauses in input formula,
each followed by white space (must match p-line of input
formula, n might only be an upper bound on the number of
variables); e.g., use printf format "%ld %ld\n".
32-255 identification, comments, etc., ASCII. It is recommended
that this section be newline-terminated, for readability.
256-end resolution proof, binary or ASCII. This section consists
of a sequence of unsigned and signed integers, according to
the format specs. The sequence is described in detail in
the next section.
The entire file is limited to 2000 megabytes (i.e., 2097152000 bytes).
This is slightly less than than 2 gigabytes to ensure that it fits in
a 2-GB file system.
The overall length limit might be increased if a program demonstrates that
it produces meaningful binary proofs that exceed this limit.
1.1. RESOLUTION PROOF FORMAT
The proof is a sequence of integers that represents the concatenation
of subsequences called PROOF OPERATIONS, where each PROOF OPERATION
consists of one of the following:
one binary resolution operation or
one unary copy operation or
one unary delete operation or
one zero-ary output operation.
Let n and m denote the number of variables and number of clauses,
as given on the p-line of the input formula.
An OPERAND is a positive unsigned integer.
An operand in the range 1-m refers to the corresponding clause in the
input formula.
A NULL OPERAND is 0, i.e., not applicable for the operation.
A CLAUSE NUMBER is a positive unsigned integer in the range 1-m.
A LABEL is a positive unsigned integer greater than m, or a clause number
in the range 1-m.
All labels for resolution or copy operations must be greater than m
and form a strictly increasing sequence.
Normaly, the first resolution or copy operation has label m+1 and
each subsequent resolution or copy operation has a label one greater than
its predecessor.
However, to facilitate proof compaction, nonconsecutive labels
are permitted.
Output and delete operations do not cause the label to increment.
A NULL LABEL is 0, and denotes an output or delete operation.
A LITERAL is a positive integer in the range 1-n or the negation of
such an integer.
A NULL LITERAL is 0, i.e., not applicable for the operation.
A CLAUSE is a subsequence consisting of one unsigned integer, say k,
followed by k literals, followed by an unsigned integer with value k again.
The value of k may be 0, denoting the empty clause.
The literals may include duplicates and/or contradictory pairs.
Notice that the clause format differs from that of DIMACS CNF files.
This format permits a program to jump over any proof operation
in either direction, in constant time.
1.2. SPECIFICATIONS OF PROOF OPERATIONS
A COPY operation consists of:
label1 0 operand1 0 clause0
where operand1 < label1.
A proof never requires a copy operation, but this capability is
provided for flexibility.
For correctness, clause0 must contain the same literals as
the clause whose label is operand1; however, the order and number of
duplicates may be different.
A RESOLUTION operation consists of:
label1 clashlit2 operand1 operand2 clause0
where operand1 < label1 and operand2 < label1.
Let clause1 be the clause whose label is operand1 and let clause2 be
the clause whose label is operand2.
For correctness, clause1 must contain the NEGATION OF clashlit2
and clause2 must contain clashlit2, and clause0 must contain
the same literals as
(clause1 less -clashlit2) union (clause2 less clashlit2)
However, the order and number of duplicates may be different.
In this notation, (clause1 less -clashlit2) means that ALL occurrences
of (-clashlit2) are deleted from clause1, and so on.
Notice that resolution involving a tautologous clause is acceptable,
although it is probably useless. Example: the resolvent of
[a, b, -c] with [c, -c, d] produces [a, b, -c, d].
Since the resolvent is subsumed by the first operand, a copy operation
would probably have been more effective.
For flexibility, duplicate literals are always treated as a single literal
in deciding correctness. For example, the resolvent of
[a, b, -c] with [b, c, c, d] may be given as [a, b, d] or [a, b, b, d]
or even [a, b, d, d] (or any permutations of these).
However, [a, b, c, d] is an error.
An OUTPUT operation consists of:
0 0 0 0.
It denotes that clause0 of the preceding copy or resolution operation is
an output clause of the proof.
This capability is included for flexibility, so that a proof can
output certain derived clauses.
The last copy or resolution operation of the file is always considered
to produce an output clause, and need not be followed by an output operation.
In normal usage, this last copy or resolution operation is the empty clause,
and the proof is a refutation.
A proof checker might stop checking after detecting a derived empty clause,
and might ignore all output operations.
A DELETE operation consists of:
0 0 operand1 0
where operand1 < label of the preceding copy or resolution operation,
or <= m if it is the first proof operation.
A proof never requires a delete operation, but this capability is
provided for flexibility.
The meaning of a delete is that operand1 will not be referenced later
in this proof.
This might permit a sophisticated proof checker to reclaim some space,
and/or detect an error.
However, a proof checker might simply ignore this operation.
1.3. EXAMPLES
EXAMPLE 1
Say the input file has these clauses (the labels are not in the file):
c example 1
p cnf 2 3
1 -2 0
1 2 0
-1 0
Thus the input clauses are referenced by 1-3.
The proof might be these integers (newlines are for readability):
4 2 1 2 2 1 1 2
5 1 3 4 0 0
This proof contains two resolution operations and implicitly outputs
the last derived clause, which is the empty clause.
EXAMPLE 2
Another correct proof for Example 1 is:
4 2 1 2 2 1 1 2
5 1 3 4 0 0
0 0 0 0
This proof contains two resolution operations and explicitly outputs
the last derived clause, which is the empty clause.
EXAMPLE 3
Another correct proof for Example 1 is:
4 0 3 0 1 -1 1
5 0 1 0 2 1 -2 2
6 0 2 0 2 1 2 2
7 2 5 6 1 1 1
0 0 5 0
0 0 6 0
8 1 4 7 0 0
0 0 0 0
This proof begins with 3 copies, possibly so it can reference
clauses according to positions in the program's own data structures.
The next operation is resolution, deriving the unit clause [1].
Then 2 delete operations occur, declaring that the proof will not
use clauses 5 and 6 anymore (possibly because clause 7 subsumes them).
Finally the proof derives the empty clause at label 8,
and explicitly outputs it.
1.4. NAVIGATION HINTS
Assume the proof is stored in an array P.
READING FORWARD
Say a proof operation begins at P[x].
If P[x] = 0, it contains exactly 4 integers and the next operation,
if any, begins at P[x + 4].
If P[x] = nonzero, then it contains at least 6 integers and
P[x + 4] contains the clause length, say L.
The total length of the proof operation is L + 6 and the next operation,
if any, begins at P[x + L + 6].
READING BACKWARD
Say a proof operation ends at P[y].
If P[y] = 0, then:
if P[y - 3] = 0, then P[y - 3] is the beginning of this
proof operation (a delete or output) and the preceding operation,
if any, ends at P[y - 4];
otherwise, this proof operation has length 6 (a resolution or copy
that produces the empty clause) and the preceding operation,
if any, ends at P[y - 6].
If P[y] = L > 0, then its total length is L + 6 and the preceding operation,
if any, ends at P[y - L - 6].
2. SPECIFICATION FOR RESOLUTION PROOF TRACE FILES (PROPOSED)
---------------------------------------------------------
The file format for a resolution proof trace is the following, where
bytes are numbered from 0, and double quotes indicate character sequences
that are NOT null-terminated:
0-3 "%RPT"
4-7 format specs, terminated by white space.
The following formats will definitely be accepted:
"L32 " denotes little-endian 32-bit (e.g., Intel);
e.g., 258 is written as 02 01 00 00 hex.
"B32 " denotes big-endian 32-bit (e.g., Sparc, MIPS);
e.g., 258 is written as 00 00 01 02 hex.
"A " denotes ASCII signed integers separated by white
space; e.g. use printf format "%ld\n".
The remaining formats are for future development:
"L64 " denotes little-endian 64-bit (e.g., Intel);
"B64 " denotes big-endian 64-bit (e.g., Sparc, MIPS);
8-31 two unsigned ASCII integers, n and m, representing the
number of variables and number of clauses in input formula,
each followed by white space (must match p-line of input
formula, n might only be an upper bound on the number of
variables); e.g., use printf format "%ld %ld\n".
32-255 identification, comments, etc., ASCII. It is recommended
that this section be newline-terminated, for readability.
256-end resolution proof, binary or ASCII. This section consists
of a sequence of unsigned and signed integers, according to
the format specs. The sequence is described in detail in
the next section.
The entire file is limited to 2000 megabytes (i.e., 2097152000 bytes).
This is slightly less than than 2 gigabytes to ensure that it fits in
a 2-GB file system.
The overall length limit might be increased if a program demonstrates that
it produces meaningful binary proofs that exceed this limit.
2.1. RESOLUTION PROOF TRACE FORMAT
The proof trace is a sequence of integers that represents the concatenation
of groups of four integers each, called TRACE OPERATIONS,
where each TRACE OPERATION consists of one of the following:
one binary resolution trace or
one unary copy trace or
one unary delete operation or
one zero-ary output operation.
The definitions given for RESOLUTION PROOF FORMAT carry over for
n, m, OPERAND, CLAUSE NUMBER, LABEL, LITERAL, and CLAUSE.
Delete and output trace operations are identical to delete and
output operations in resolution proof format.
Resolution and copy trace operations each have an implicitly
associated clause (whereas the clause is explicit in resolution proof
format).
2.2. SPECIFICATIONS OF TRACE OPERATIONS
A COPY trace consists of:
label1 0 operand1 0
where operand1 < label1.
The clause associated with label1 is a clause that contains the
same literals as the clause associated with operand1.
A proof never requires a copy operation, but this capability is
provided for flexibility.
A RESOLUTION trace consists of:
label1 clashlit2 operand1 operand2
where operand1 < label1 and operand2 < label1.
Let clause1 be the clause associated with operand1 and let clause2 be
the clause associated with operand2.
For correctness, clause1 must contain the NEGATION OF clashlit2
and clause2 must contain clashlit2.
The clause associated with label1 contains the same literals as
(clause1 less -clashlit2) union (clause2 less clashlit2),
that is, it is the resolvent of clause1 and clause2, using clashlit2
as the clashing literal. See the discussion under resolution proof format
for additional details.
2.3. EXAMPLES
EXAMPLE 4
Say the input file (DIMACS format, repeated from Example 1) is:
c example 1
p cnf 2 3
1 -2 0
1 2 0
-1 0
Thus the input clauses are referenced by 1-3.
The trace might be these integers (newlines are for readability):
4 2 1 2
5 1 3 4
This trace contains two resolution traces and implicitly outputs
the last derived clause, which is the empty clause.
3. REMARKS
-------
The purpose of the resolution proof format is to enable the proof checker
to identify a specific operation as an error, if an error occurs.
The resolution proof trace format can only determine that an error
has occurred somewhere, if an operand of resolution fails to contain
the clashing literal, but this might be many steps later than the
deviation between the solver and the proof trace checker.
In the worst case, at the end of the proof trace, the proof trace checker
finds that the final clause is not empty and no error has been detected.
A solver might choose to output the resolution proof trace to save time
and space.
In this case, it is the ``overall'' solver's responsibility to run
a postprocesser to produce the resolution proof format for the checker.
The ``overall'' solver might be a script or other control program
that invokes the actual solver, then invokes the postprocesser.
Either a proof or proof trace might be subjected to post-analysis
to delete irrelevant operations.
Clearly, the fixed format of the proof trace is more convenient for
reachability analysis.
The organizers of the SAT05 solver competition expect to provide
programs to convert a proof trace format into a proof format and
to check correctness of a proof format.
They expect to provide options or converters for L32, B32, and A formats.
These programs will be designed for a unix environment, such as
Linux, Solaris, etc., and will be written to work on both big-endian
and little-endian machines (without knowing which type the machine is).
In some cases, unix features might be used to improve the processing
of very large files, such as pipes, mmap, and forks.
The design should be such that specialized features are confined
to subroutines that can be replaced with less specialized
implementations, at the cost of performance and size limitations.
The trace-to-proof converter program is provided as a courtesy and
used at the submitter's own risk.
In particular, any submitter's solver might output its own
intermediate file format.
The proof trace format proposed here is not required.
The proof checker itself will be used by the competition organizers
to evaluate resolution proofs produced by solvers.