How well does it work?
Compare tididi-cnf with decision-diagram compilers, logic-circuit compilers and model counters on all 1,400 MCC 2020–2026 track-1 entries, with two minutes per instance. Method · Supplementary data · Try the compiler
Solved per set
Solved within a time limit
Time runs horizontally; instances solved run vertically. A point at t seconds and n instances means the solver finished n instances in t seconds or less each. Higher is better. Point at a curve, or focus the plot and use the arrow keys, to read it; the buttons show and hide each solver.
Head to head
One point per instance either solver solved, at the time each took; the diagonal is where they take the same.