WDIMACS Input format

The input file is given as an argument. For example:

./maxhs <input_file_name>

The input file can optionally be gzipped:

./maxhs <input_file_name>.gz;

Unweighted Max-SAT with no hard clauses input format

c unweighted Max-SAT with no hard clauses
c This is the same input format used for ordinary SAT problems
c
p cnf 3 4
1 -2 0
-1 2 -3 0
-3 2 0
1 3 0

• The file can start with comments, that is lines beginning with the character 'c'.
• Right after the comments, there is the line "p cnf nbvar nbclauses" indicating that the instance is in CNF format; nbvar is the number of a variables appearing in the file; nbclauses is the exact number of clauses contained in the file.
• Then the clauses follow. Each clause is a sequence of non-zero integer numbers between -nbvar and nbvar ending with 0 on the same line. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.

Weighted Max-SAT input format

In Weighted Max-SAT, the parameters line is "p wcnf nbvar nbclauses". Clauses are expressed as above, except that there the first number of each clause line identifies the weight of the clause. This number can be expressed in floating point or it can be an integer. The number must be greater than zero. Note that many other Max-SAT solvers require this number to be an integer

Example of Weighted Max-SAT formula:

c
c comments Weighted Max-SAT
c
p wcnf 3 4
10 1 -2 0
3 -1 2 -3 0
0.8 -3 2 0
5.6 1 3 0

Weighted Partial Max-SAT input format

In Weighted Partial Max-SAT, the parameters line is "p wcnf nbvar nbclauses top". As above with weighted Max-Sat each clause has a weight specified by the first number of each clause line. top is a marker for hard clauses. When the clause weight is equal to top the clause is considered to be a hard clause. Thus top on the "p-line" should be a number large enought that no soft-clause will have that weight. Furthermore, many Max-SAT solvers require that top be larger that the sum of the weights of the falsified clauses in an optimal solution (top being the sum of the weights of all soft clauses plus 1 will always suffice).

Example of Partial Max-SAT formula:

c
c comments Partial Max-SAT
c
p wcnf 4 5 15
15 1 -2 4 0
15 -1 -2 3 0
2 -2 -4 0
5 -3 2 0
3 1 3 0

Output format

maxhs writes to standard out using the following types of lines

• Comments ("c " lines):
  These lines start by the two characters: lower case 'c' followed by a space (ASCII code 32).
  These lines contain information about maxhs's progress. Use --verb=0 if you do not want any such output


• optimal solution ("o " line):
  If maxhs can solve the problem it will output one line starting with lower case 'o' followed by a space (ASCII code 32) followed by a number which represents the cost of an optimal solution, i.e., the sum of the weights of the unsatisfied clauses in the optimal solution.


• Solution ("s " line):
  If maxhs can solve the problem it will output one line
  

  s OPTIMUM FOUND



• Values ("v " lines):
  If maxhs can solve the problem (or if you use the flag "-printBstSoln") maxhs will output a v-line specifying the found truth assignment (best solution found). These lines start with the lower case 'v' followed by a space (ASCII code 32).
  The following numbers will be a list of literals that are true in the reported solution.
  A literal is denoted by an integer that identifies the variable and the negation of a literal is denoted by a minus sign immediately followed by the integer of the variable.
  

Example

c MaxHS 2.9.0
c Muser added 831 hard clauses
c IBM CPLEX version 12.6.3.0
c Init Bnds: SAT Time 0
c Init Bnds: LB = 0 UB = 71696
c Bnds: LB = 68579 UB = 71486
c Solved by Cplex Model
o 68579
s OPTIMUM FOUND
v 1 -2 -3 -4 -5 6 -7 -8 -9 -10 11 -12 -13 -14 15 -16 -17 -18 -19 -20 -21 22 -23 24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 37 -38 -39 -40 -41 42 -43 -44 -45 -46 -47 48 -49 50 -51 -52 -53 54 -55 -56 -57 -58 -59 60 -61 -62 -63 -64 -65 66 -67 -68 69 -70 -71 -72 -73 -74 75 -76 -77 -78 -79 -80 81 82 -83 84 -85 -86 -87 88 -89 -90 91 -92 -93 -94 95 -96 -97 -98 -99 -100 -101
c Solved: Number of falsified softs = 80
c CPLEX: #constraints 880
c CPLEX: Avg constraint size 2
c CPLEX: #non-core constraints 0
c CPLEX: Ave non-core size -nan
c SAT: #calls 54
c SAT: Total time 0
c SAT: #muser calls 0 (-nan % successful)
c SAT: Minimize time 0 (-nan%)
c SAT: Avg constraint minimization 0
c CPLEX: #calls 1
c CPLEX: Total time 0.007444
c GREEDY: #calls 0
c GREEDY: Total time 0
c MEM MB: 28
c CPU: 0.011781