A C++ tool for extracting data from SAT solvers or bounded model checkers output into csv format. It supports various solvers including ParaFROST or MiniSat and the bounded model checker CBMC. Information like the running time, Satisfiability result or solving statistics will be parsed into a comma-separated file.
As input, it reads a log file generated by the solver if the file had the prefix "result_" and the extension ".txt". More prefixes can be supported.
A table in comma-separated CSV format.
Run the tool on the test folder (contains logs from parafrost and minisat solvers) using the commad:
sat2csv test -s test_results
where "test" is the directory name containing the log files, "-s" instructs the tool to extract a SAT solver information, and "test_results" is the name of the CSV file. The output file produced will look like this:
| CNF | Simplify time (s) | Solve time (s) | Sat. |
|---|---|---|---|
| 01-integer-programming-20-30-40 | 4.242 | 3201.933 | S |
| 9dlx_vliw_at_b_iq1 | 0 | 19.5243 | U |
The "S" and "U" letters denote "SATISFIABLE" and "UNSATISFIABLE" respectively.
Run compile.sh inside sat2csv on a Linux-based machine or compile the sources on Windows with any C/C++ compiler to produce the binary sat2csv. For more help on the available options use "-h".