search

sat-group / open-wbo

Open-WBO: state-of-the-art MaxSAT and Pseudo-Boolean solver
Other
69 stars 12 forks source link

Understanding output and recovering unsatisfied clauses #3

Closed dhruvparamhans closed 6 years ago

dhruvparamhans commented 6 years ago

Would it be possible to edit the README a bit so as to understand the output of the program. In particular when running on a .cnf file which I know has non-zero number of unsatisfied clauses, what do the lines starting with "o" (followed by a number) mean.

Furthermore, is there an easy way to recover the index of the clauses that are unsatisfied? For the moment, the program outputs the assignment of each of the variables.

Thanks.

rubengmartins commented 6 years ago

Thanks for the suggestion. We will clarify in the README the output of the solver.

Note that Open-WBO follows the standard notation of MaxSAT solvers. More information can be found in the paper "The First and Second Max-SAT Evaluations" (https://satassociation.org/jsat/index.php/jsat/article/viewFile/53/47)

Current optimal solution ("o" lines): These lines, which are mandatory, start by lower case "o" followed by a space and then by an integer which represents the lowest number of clauses falsified so far by an assignment. The evaluation environment will take as optimal number of unsatisfied clauses the last "o" line in the output stream.

Regarding your second comment:

Furthermore, is there an easy way to recover the index of the clauses that are unsatisfied? For the moment, the program outputs the assignment of each of the variables.

I can add an option to print the unsatisfied soft clauses in the optimal solution instead of the assignment. Would this work for you?

dhruvparamhans commented 6 years ago

Thank you for the quick reply. Thank you for the reference.

Apropos the unsatisfied clauses, it would be great to have that option. Ideally, it would be great to have both: the assignment and the unsatisfied clauses (if its not too much work)

Thanks once again.

rubengmartins commented 6 years ago

I updated the code to include an option that allows writing the unsatisfied clauses to a file. Since the number of soft clauses may be large, I think this is a better option than printing it directly to the output.

You can use the new option with: ./open-wbo -print-unsat-soft=<filename-unsat-soft> <filename>

I also updated the README.md with your suggestions.

dhruvparamhans commented 6 years ago

Thank you. I just checked and it works like a charm. I have another question, but perhaps its better to open a new issue.

I shall close this one.