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;
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
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
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
maxhs writes to standard out using the following types of lines
s OPTIMUM FOUND
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