|
1 | | -# README for the Open-WBO MaxSAT Solver |
2 | | -## Version 2.1 -- September 2018 |
| 1 | +# Open-WBO MaxSAT Solver |
| 2 | +## Version 2.1 - September 2018 |
3 | 3 |
|
4 | 4 | Open-WBO is an extensible and modular open-source MaxSAT Solver. |
5 | 5 | Open-WBO was one of the best solvers in the partial MaxSAT categories at |
6 | 6 | MaxSAT Evaluations 2014, 2015, 2016 and 2017 and in the decision and |
7 | 7 | optimization for SMALLINT categories at PB Evaluation 2016. |
8 | 8 |
|
9 | 9 | ## MaxSAT Evaluation 2018 |
10 | | -### The default algorithms used by Open-WBO in the complete track are: |
11 | | -### unweighted: Part-MSU3 ; weighted: OLL |
| 10 | +The default algorithms used by Open-WBO in the complete track are: |
| 11 | +* unweighted: Part-MSU3 |
| 12 | +* weighted: OLL |
12 | 13 |
|
13 | 14 | Usage of the solver: |
14 | 15 | ./open-wbo [options] <input-file> |
@@ -65,18 +66,20 @@ The following options are available in Open-WBO: |
65 | 66 | Open-WBO follows the standard output of MaxSAT solvers: |
66 | 67 | * Comments ("c " lines) |
67 | 68 | * Solution Status ("s " line): |
68 | | -..* s OPTIMUM FOUND : an optimum solution was found |
69 | | -..* s UNSATISFIABLE : the hard clauses are unsatisfiable |
70 | | -..* s SATISFIABLE : a solution was found but optimality was not proven |
| 69 | + * s OPTIMUM FOUND : an optimum solution was found |
| 70 | + * s UNSATISFIABLE : the hard clauses are unsatisfiable |
| 71 | + * s SATISFIABLE : a solution was found but optimality was not proven |
71 | 72 | * Solution Cost Line ("o " lines): |
72 | | -..* This represents the cost of the best solution found by the solver. The cost |
73 | | -of a solution is given by the sum of the weights of the unsatisfied soft clause. |
| 73 | + * This represents the cost of the best solution found by the solver. The cost |
| 74 | + of a solution is given by the sum of the weights of the unsatisfied soft clause. |
74 | 75 | * Solution Values (Truth Assignment) ("v " lines): |
75 | | -..* This represents the truth assignment (true/false) assigned to each variable. |
76 | | -A literal is denoted by an integer that identifies the variable and the negation |
77 | | -of a literal is denoted by a minus sign immediately followed by the integer of |
78 | | -the variable. |
| 76 | + * This represents the truth assignment (true/false) assigned to each variable. |
| 77 | + A literal is denoted by an integer that identifies the variable and the negation |
| 78 | + of a literal is denoted by a minus sign immediately followed by the integer of |
| 79 | + the variable. |
79 | 80 |
|
80 | 81 | > Authors: Ruben Martins, Vasco Manquinho, Ines Lynce |
| 82 | +
|
81 | 83 | > Contributors: Miguel Neves, Norbert Manthey, Saurabh Joshi, Mikolas Janota |
| 84 | +
|
82 | 85 | > To contact the authors please send an email to: open-wbo@sat.inesc-id.pt |
0 commit comments