Broken LRAT (and potentially other) output on Windows

[hargoniX]

Consider the following UNSAT CNF:

p cnf 43 9
43 0
-43 1 0
-43 -42 0
43 -1 42 0
-42 -10 0
-42 -10 0
42 10 10 0
-10 0
1 0

Solving this with cadical 1.9.5 like so:

cadical in.cnf foo.lrat --lrat --binary=true --quiet --unsat

Yields a fine binary UNSAT proof on Linux. However on Windows the output ends up getting corrupted.

Hexdump Linux:

0000000 1461 0002 0402 6400 0004 1661 0055 0602
0000010 6400 0806 0c0a 6100 1418 1600 000e 0e64
0000020 6100 001a 1018 0000
0000027

Hexdump Windows:

0000000 1461 0002 0402 6400 0004 1661 0055 0602
0000010 6400 0806 0a0d 000c 1861 0014 0e16 6400
0000020 000e 1a61 1800 0010
0000028

The reason for this becomes more apparent when running hexdump -c to do some ASCII decoding.

Linux:

0000000   a 024 002  \0 002 004  \0   d 004  \0   a 026   U  \0 002 006
0000010  \0   d 006  \b  \n  \f  \0   a 030 024  \0 026 016  \0   d 016
0000020  \0   a 032  \0 030 020  \0
0000027

Windows:

0000000   a 024 002  \0 002 004  \0   d 004  \0   a 026   U  \0 002 006
0000010  \0   d 006  \b  \r  \n  \f  \0   a 030 024  \0 026 016  \0   d
0000020 016  \0   a 032  \0 030 020  \0
0000028

As you can observe the proof contains a literal identifier that, just by chance, happens to be ASCII equivalent to \n. On Windows this is expanded to \r\n automatically by libc APIs. This can presumably be fixed by inserting O_BINARY at the appropriate locations in the solver. Note that this behavior also breaks other output formats. For example the clear text LRAT one should contain \n as a newline delimiter according to https://www.cs.utexas.edu/~marijn/publications/lrat.pdf but does instead contain \r\n due to (presumably) the same reason.

Unfortunately this makes using the binary LRAT format reliably for Windows applications (my specific use case runs on both Linux and Windows system) impossible.

[a1880]

This could probably be cured by changing file.cpp near line 185:

FILE *File::write_file (Internal *internal, const char *path) {
  MSG ("opening file to write '%s'", path);
#ifdef __WIN32
  return open_file (internal, path, "wb");
#else
  return open_file (internal, path, "w");
#endif
}

I am not sure, if this routine is also called for text files.

[m-fleury]

The function is called for writing proofs (DRAT, LRAT, veriPB) but also in dump_cnf and write_extension for debugging (text only).

• DRAT and LRAT use '\n' only.
• veriPB: I did not see it in https://satcompetition.github.io/2023/downloads/proposals/veripb.pdf
• For DIMACS (dump_cnf), I do not think that the sort of line break is specified (https://web.archive.org/web/20190325181937/https://www.satcompetition.org/2009/format-benchmarks2009.html)
• For printing the extension, I do not know if there is a format for that or not.