MC-2020 Competition Format

Track 1: Model Counting

Solver submissions for this track should output for a given Boolean formula the model count of the instance.

Input Instance Format

Input files are given in DIMACS CNF format.

DIMACS CNF (.cnf)

• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Variables are consecutively numbered from 1 to n
• Problem description
  • Form “p cnf NumVariables NumClauses”
    • Line starting with character p
    • followed by the problem descriptor cnf
    • followed by number n of variables
    • followed by number m of clauses
    • each separated by space each time
  • Unique (No other line may start with p)
  • Has to be the first line (except comments)
• Remaining lines indicate clauses
  • consisting of decimal integers separated by space
  • Lines are terminated by character “0”
  • Line “2 -1 3 0\n” indicates the clause “2 or not 1 or 3”
• Empty lines or lines consisting of spaces may occur and only will be ignored

Example:

c This file describes a DIMACS CNF in MC 2020 format with 6 variables and 4 clauses 
p cnf 6 4
-1 -2 0
2 3 -2 0
c this is a comment and will be ignored
4 5 0
4 6 0

Output Format (.mc)

• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Vertices are consecutively numbered from 1 to n
• Solution description
  • Form “s mc numSolutions”
    • Line starting with character s
    • followed by the problem descriptor mc
    • followed by number numSolutions indicating the model count
    • each separated by space each time
  • Unique (No other line may start with s)
  • Has to be the first line (except comments)
• Empty lines or lines consisting of spaces may occur and only will be ignored

c This file describes that the model count is 30
s mc 30

Instances

TBA

Track 2: Weighted Model Counting

Solver submissions for this track should output for a given Boolean formula, and a weight function, the weighted model count of the instance.

Input Instance Format

Input files are given in Weighted CNF format, which is a slight extension of DIMACS CNF format.

Weighted CNF (.wcnf)

• Format as DIMACS CNF
• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Variables are consecutively numbered from 1 to n
• Problem description
  • Form “p wcnf NumVariables NumClauses”
    • Line starting with character p
    • followed by the problem descriptor cnf
    • followed by number n of variables
    • followed by number m of clauses
    • each separated by space each time
  • Unique (No other line may start with p)
  • Has to be the first line (except comments)
• Weight function
  • Lines of the form “w Literal Weight 0”
  • Defines the floating point Weight for Literal, where 0 <= Weight <= 1
  • We do not use more than 9 significant digits after the decimal point
  • If the weight for a literal is not defined, it is considered to be of weight 1
• Remaining lines indicate clauses
  • consisting of decimal integers separated by space
  • Lines are terminated by character “0”
  • Line “2 -1 3 0\n” indicates the clause “2 or not 1 or 3”
• Empty lines or lines consisting of spaces may occur and only will be ignored

Example:

c This file describes a weighted CNF in MC 2020 format with 6 variables and 4 clauses 
p wcnf 6 4
w 1 0.4 0
w -1 0.6 0
w 4 0.5 0
w -4 0.5 0
w 5 1.0 0
w -5 1.0 0
-1 -2 0
2 3 -2 0
c this is a comment and will be ignored
4 5 0
4 6 0

Output Format (.wmc)

• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Vertices are consecutively numbered from 1 to n
• Solution description
  • Form “s wmc numSolutions”
    • Line starting with character s
    • followed by the problem descriptor wmc
    • followed by number numSolutions indicating the weighted model count
    • each separated by space each time
  • Unique (No other line may start with s)
  • Has to be the first line (except comments)
• Empty lines or lines consisting of spaces may occur and only will be ignored

c This file describes that the weighted model count is 8.0
s wmc 8.0

Track 3: Projected Model Counting

Solver submissions for this track should output, for a given Boolean formula and set of projection variables, the projected model count of the instance.

Input Instance Format

Input files are given in Projected CNF format, which is a slight extension of DIMACS CNF format.

Projected CNF (.pcnf)

• Format as DIMACS CNF
• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Variables are consecutively numbered from 1 to n
• Problem description
  • Form “p pcnf NumVariables NumClauses”
    • Line starting with character p
    • followed by the problem descriptor cnf
    • followed by number n of variables
    • followed by number m of clauses
    • followed by number of projected variables
    • each separated by space each time
  • Unique (No other line may start with p)
  • Has to be the first line (except comments)
• Set of projected variables
  • Line of the form “vp VARID1 VARID2 VARID3 0”
  • Unique (No other line may start with vp)
  • Line may occur at any time after the p line, esp. also as last line in the file
  • Defines the projected variables, i.e., variables that are important and which are the ones that will be considered for the count
  • Consisting of decimal integers separated by space
  • Lines are terminated by character “0”
  • Line “vp 1 2 0\n” indicates the set {1, 2} of projection variables
  • 1 <= VARID <= n (n… number of variables)
• Remaining lines indicate clauses
  • consisting of decimal integers separated by space
  • Lines are terminated by character “0”
  • Line “2 -1 3 0\n” indicates the clause “2 or not 1 or 3”
• Empty lines or lines consisting of spaces may occur and only will be ignored

Example:

c This file describes a projected CNF in MC 2020 format with 6 variables and 4 clauses and 2 projected variables 
p pcnf 6 4 2
vp 1 2 0
-1 -2 0
2 3 -2 0
c this is a comment and will be ignored
4 5 0
4 6 0

Output Format (.pmc)

• Line separator ‘\n’
• Lines starting with character c are interpreted as comments
• Vertices are consecutively numbered from 1 to n
• Solution description
  • Form “s pmc numSolutions”
    • Line starting with character s
    • followed by the problem descriptor pmc
    • followed by number numSolutions indicating the projected model count
    • each separated by space each time
  • Unique (No other line may start with s)
  • Has to be the first line (except comments)
• Empty lines or lines consisting of spaces may occur and only will be ignored

c This file describes that the projected model count is 3
s pmc 3