D4 is a library designed to compute model counts of logical formulas. It currently supports CNF and circuit-based formats, and can be integrated into custom applications for advanced reasoning and model enumeration tasks.

This README provides an overview of how to use the D4 library, the supported input formats, and example usage.

D4 supports various methods to analyze and count models of logical formulas. More detailed documentation on the methods used internally (e.g., decision diagrams, SAT solvers, etc.) will be added soon.

D4 is implemented as a library and should be linked into a separate executable for use. A demo executable is provided to demonstrate basic functionality.

To run a simple counter example on a CNF file:

cd demo/counter
./build.sh
./build/counter -i ../../instancesTest/cnfs/cnf5.cnf

To count models of a circuit-based input, see the example under the circuit section below.

D4 supports a custom circuit format (BC-S1.2), where formulas are defined in terms of logic gates and evaluation constraints. This format allows complex Boolean functions to be represented more directly than CNF.

A BC-S1.2 file consists of:

• Comments: Prefixed with c
• Weight Information (optional): c w <literal> <weight>
• Input Variables: I <var>
• Gate Definitions: G <var> := <formula>
• Target Literals: T <literal>

A gate's formula can be one of:

• A <lit1> <lit2> ... – AND
• O <lit1> <lit2> ... – OR
• I <lit> – Identity (can also represent negation using -<lit>)

A literal is either a variable or its negation (e.g., x, -x).

c BC-S1.2
I x
T -x

c BC-S1.2
I a
I b
I c
G g1 := A a b
G g2 := A -c b
G g3 := O g1 -g2
T g3

To run the model counter on a circuit:

./build/counter -i ../../instancesTest/circuits/circ1.bc --input-type circuit

D4 also supports the standard DIMACS CNF format. This is widely used in SAT solving and describes Boolean formulas as a conjunction of clauses, each a disjunction of literals.

To run a model counter on a CNF file:

./build/counter -i ../../instancesTest/cnfs/cnf5.cnf