File formats used by optimization programs.

Formats for min-cost sat

cnf format, extension .cnf

• multiple comment lines of the form c COMMENT_TEXT
• a single tag line of the form p cnf VARS CONSTRAINTS
• multiple constraints of the form
  s₁ s₂ ... s_k 0
  A constraint can span multiple lines (some scripts may work only when each constraint occupies a single line).
  Each s_j is an integer k other than 0.
  If k > 0, then variable k appears in the constraint with a coefficient of 1.
  If k < 0, then variable |k| appears in the constraint with a coefficient of -1.

  It is assumed that |k| is at most the value of VARS in the tag line and the number of constraints is at most CONSTRAINTS.

cnfx format, extension .cnfx

There are two differences from cnf format:

1. The tag line is p cnfx VARS CONSTRAINTS
2. After the tag line and before the list of constraints, there is a list of pairs i₁ w₁ i₂ w₂ .... A pair i_k w_k means that variable i_k has weight w_k.
   Any variable not appearing among the pairs has weight 0. The list of pairs ends with the pair 0 0.
   Each pair can be on a different line or any number can be on a single line.

lpx format, extension .lpx

There are several fundamental differences between lpx and cnf, since the former needs to address general optimization problems.

• Variables can have arbitrary names, not just integers; variable names begin with letters and have any number of letters or digits.
• There is an explicit statement of the linear expression to be optimized.
• The notation is algebraic for both the expression to be optimized and the constraints.
• Variables must be identified specifically as 0/1 (binary).

• multiple comment lines of the form \ COMMENT_TEXT. In contrast to cnf format, these comments can be anywhere in the file.
• the keyword Min (since this is a minimization problem)
• the expression to be optimized written as a linear form.
• multiple constraints, each of which is a linear form, followed by a relational operator -- one of <, =, >, <=, >= -- and a numerical constant, for example
  x1 - 3 x2 + x3 <= -1
• the keyword Binary (since the variables are 0/1)
• a list of all the variables separated by white space
• the keyword End

An example showing both cnfx and lpx format

c A weighted set cover instance.
c InstanceProfile:  
c   nVars=8, nClauses=5 
c   nLitsPos=5 nLitsNeg=0  nLitsTot=5  ImbalanceOfLits=1   
c 
c Variable weights - x1: 6, x2: 12, x3: 10, x4: 8
c                    x5: 5, x6:  7, x7:  3, x8: 3
p cnfx 8 5 

1 6
2 12
3 10
4 8
5 5
6 7
7 3
8 3
0 0

1 2 4 7  0
1 2 3 5 8  0
2 3 4 6  0
5 7 0
6 8 0

\  File sample.lpx, created Wed Jun 06 02:16:47 UTC 2007
\   - created from covering/sat instance sample.cnfx
\  A weighted set cover instance.
\  InstanceProfile:
\  nVars=8, nClauses=5
\  nLitsPos=5 nLitsNeg=0 nLitsTot=5 ImbalanceOfLits=1
\  
\  Variable weights - x1: 6, x2: 12, x3: 10, x4: 8
\  x5: 5, x6: 7, x7: 3, x8: 3
\  5 rows, 8 columns
Min
  obj: +6 x1 +12 x2 +10 x3 +8 x4 +5 x5 +7 x6 +3 x7 +3 x8

st
  c1: +x1 +x2 +x4 +x7 >= 1
  c2: +x1 +x2 +x3 +x5 +x8 >= 1
  c3: +x2 +x3 +x4 +x6 >= 1
  c4: +x5 +x7 >= 1
  c5: +x6 +x8 >= 1
Binary
   x1 x2 x3 x4 x5 x6 x7 x8
End