tididi-cnf is a knowledge compiler and model counter for CNF.
Paste a DIMACS CNF, open or drop a file, or pick an example: tididi-cnf
compiles the formula into a Tree Decision Diagram and counts its models: the model count, the weighted count, or either one projected
onto the formula's show variables. The weights and the show variables come
from the formula's own c p weight and c p show
lines, and its c t line names the task unless you pick one.
Everything runs in this tab and nothing is uploaded. tididi-cnf is also a
Rust crate with a
command-line tool and
API
documentation; its
input
reference describes the format, and its evaluation
compares it with decision-diagram compilers, logic-circuit compilers and
model counters.
Input
Result
This result is for an earlier input or earlier settings.Press Run.
The run's record, as tididi --stats writes it
Progress, as the binary prints it on stderr
Watch it compile
This drawing is for an earlier input.tididi-cnf compiles a formula bottom-up over a vtree, a binary tree with one variable at each leaf, into a Tree Decision Diagram. Each clause waits at the lowest vtree node whose subtree holds all its variables. At each node, the diagrams of its two sides are joined, and the clauses waiting there are conjoined in. A diagram node is the disjunction of its pairs, and a pair, drawn as a box of two halves, is the conjunction of a function of the variables on the left and one of those on the right; ⊤ stands for a side that every assignment satisfies. Beside each node is the number of assignments to its variables that satisfy it: a pair multiplies its two sides and a node adds its pairs, which is the whole of counting.
Ask the diagram
The drawing compiles the formula as it is written, on the vtree vitri's portfolio builds for it, for a formula of a few variables. The count above runs the whole pipeline: it preprocesses the formula first, and projects onto the show variables of a projected task, which the drawing does not.