INPUT TYPES

The input files must follow the DIMACS format for these instances. There are three possible variations:

Type 1: Simple Max Sat instances

The weight of all clauses is 1. Therefore the objective is to find an assignment of the variables that maximizes the total number of satisfied clauses.

Type 2: Weighted Max Sat instances

Each clause has an arbitrary integer weight in the range [1,2²⁰]. The objective is to find an assignment that provides the maximum total weight of the satisfied instances.

Type 3: Partial Max Sat instances

This is similar to the type of Weighted Max Sat instances, but the clauses are partitioned into two groups: the soft clauses and the hard clauses. The objective is to find an assignment that satisfies all hard clauses and provides the maximum total weight of the satisfied soft instances.

SYNTAX RULES

Here are the rules that the user should follow to edit the input file. An instance is described by the following three sections that must appear in the order shown:

a) Comment section

1. The section is optional and should be used to give additional information concerning the instance (the name, the source, a general description, and the like)
2. Each line of the section starts with the letter “c” (lower case)
3. The section is made of an arbitrary number of consecutive lines

b) Problem section

1. The section is used to describe the problem type
2. The section is made of a single line that starts with the letter “p” (lower case)
3. The line format is one of the following:
   • Type 1: p cnf <nvar> <ncl>
   • Type 2: p wcnf <nvar> <ncl>
   • Type 3: p wcnf <nvar> <ncl> <thresh>

where <nvar> is a positive integer that gives the number of variables, <ncl> is a positive integer that gives the number of clauses, and <thresh> is an integer larger than the sum of the weights of all soft clauses. These fields are separated by blank or by TAB characters

c) Clause section

1. The section is used to describe each clause of the instance. Each variable in the instances is referenced with an integer in the range [1,<nvar>]. A variable with name in the range [1,<nvar>] does not have to appear necessarily in some of the clauses. Negated variables have their name preceded by a “-” sign
2. The section is made of as many records as the number of clauses in the instance (<ncl>). Each record must start with a new line and must terminate with the parameter 0. All following characters before the end of line are not processed and thus can be used for comments
3. The record format is one of the following:
   • Type 1: <variables> 0
   • Type 2 and 3: <weight> <variables> 0

where <variables> is a list fields, each of them corresponding to the name of a variable, possibly preceded by the “-” sign, and <weight> is an integer in the range [1,2²⁰] representing the weight of the clause. For Type 3, soft clauses have weight less than <thresh>, the others are hard clauses. The fields in the record are separated by blank, TAB, or NEW-LINE characters; therefore, a record describing a clause can span more than one line.

EXAMPLES

Instance of Type 1:

maximize (x₁ OR ¬ x₂ OR x₄) + (¬ x₁ OR ¬ x₃ OR x₄ OR x₆ OR x₇) + (¬ x₁ OR ¬ x₄)

Input file:

c

c Max Sat instance

c

p cnf 7 3

1 -2 4 0

-1 -3 4 6 7 0

-1 -4 0

Instance of Type 2:

maximize 6 (x₁ OR ¬ x₂ OR x₄) + 5 (¬ x₁ OR ¬ x₃ OR x₄ OR x₆ OR x₇) + 2 (¬ x₁ OR ¬ x₄)

Input file:

c

c Weighted Max Sat Instance

c

p wcnf 7 3

6 1 -2 4 0

5 -1 -3 4 6 7 0

2 -1 -4 0

Instance of Type 3:

maximize 6 (x₁ OR ¬ x₂ OR x₄) + 5 (¬ x₁ OR ¬ x₃ OR x₄ OR x₆ OR x₇)

subject to (¬ x₁ OR ¬ x₄) = 1

Input file:

c

c Partial Weighted Max Sat instance

c

p wcnf 7 3 14

6 1 -2 4 0

5 -1 -3 4 6 7 0

14 -1 -4 0