GET IN TOUCH
MC 2020

Competition Tracks / Formats

The challenge consists of two separate tracks:

  1. Model Counting (mc), and
  2. Weighted Model Counting (wmc)
  3. Projected Model Counting (pmc)

Note that we only allow non-parallel solvers. For more details on active calls for benchmark instances and participation, we refer to Submission & Important Dates.

Benchmark Instances

There will be 200 benchmark instances for each track, labeled (p|w)mc_001.(p|w)cnf to (p|w)mc_200.(p|w)cnf for the track on (P|W)MC, respectively.

Larger numbers in the filename should (as a rule of thumb) correspond to harder instances. The odd instances are public and the even instances will be provided later (secret).

Submission (optil)

We refer to a more detailed subpage.

Evaluation (optil)

  • timeout: 15 minutes per instance
  • in detail: 900s (soft cpu), 905 (hard cpu), 1000 (soft wall), 1005 (hard wall)
  • Output: 524288 B
  • Mem: 8,388,608 KB
  • measure: number of solved instances
  • objective: minimize the measure

Evaluation (private instances / Track 1 and 2)

  • timeout: 30 minutes per instance
  • Environment: either on Taurus or a cluster running an Ubuntu 16.04 LTS (kernel 4.4.0-166-generic, gcc 5.4.0)
  • in detail: 1800s (soft cpu), 1805 (hard cpu), 1900 (soft wall), 1905 (hard wall)
  • Output: 524288 B
  • Mem: 8,388,608 KB
  • measure: number of solved instances
  • objective: minimize the measure

Evaluation (private instances / Track 3)

  • timeout: 60 minutes per instance
  • Environment: either on Taurus or a cluster running an Ubuntu 16.04 LTS (kernel 4.4.0-166-generic, gcc 5.4.0)
  • in detail: 3600s (soft cpu), 3605 (hard cpu), 3700 (soft wall), 3705 (hard wall)
  • Output: 524288 B
  • Mem: 8,388,608 KB
  • measure: number of solved instances
  • objective: minimize the measure

Track 1: Model Counting

Solver submissions for this track should output for a given Boolean formula the model count of the instance. For more details of the problem, we refer to Model Counting. If the solver does not output the exact model count - the solver will not be disqualified, which ensures that we do not require arbitrary precision.

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. For more details of the problem, we refer to Weighted Model Counting. The provided weighted model count does not have to be exact, but we expect 1% accuracy.

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. For more details of the problem, we refer to Projected Model Counting. If the solver does not output the exact projected model count - the solver will not be disqualified, but the instance will count as not solved. This ensures that we do not require arbitrary precision.

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

Instances

TBA