/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.