d4Solver 0.1.0

Python bindings for the D4 model counter and compiler

py-d4

Python bindings for the D4 compiler and model counter, supporting option structures, CNF files, custom clause vectors, logic circuits, weighted model counting, and d-DNNF queries. Built with nanobind and scikit-build-core.

---

🚀 Users Guide

1. Installation

Install the package directly from your GitLab PyPI package registry (typically configured in your CI or local .pip/pip.conf):

pip install d4Solver --extra-index-url https://gitlab.univ-artois.fr/api/v4/projects/<PROJECT_ID>/packages/pypi/simple

2. Usage Examples

2.1 Basic Model Counting

You can instantiate a Solver using a CNF filepath or raw Python clause structures (list of lists/tuples of literals, 1-based indexing):

import py_d4

# 1. Option A: Load from a DIMACS CNF file
solver = py_d4.Solver("path/to/formula.cnf")

# 2. Option B: Pass raw Python clauses and total variable count
# Formula: (x1 or x2) and (not x2 or x3)
clauses = [
    [1, 2],
    [-2, 3]
]
nb_vars = 3
solver = py_d4.Solver(clauses, nb_vars)

# Run model counting
count_res = solver.count()
print(f"Number of models: {count_res.getResult()}")     # Large integer as string (GMP support)
print(f"As Python integer: {count_res.getIntResult()}")  # Safe python int

2.2 Compilation to d-DNNF

py-d4 can compile CNF formulas and circuits into Decision Diagram / Deterministic Decomposable Negation Normal Form (d-DNNF):

import py_d4

clauses = [[1, 2], [-2, 3]]
solver = py_d4.Solver(clauses, 3)

# Compile
compile_res = solver.compile()

# Access compiled graph statistics
print(f"Nodes in d-DNNF: {compile_res.getNbNodes()}")
print(f"Edges in d-DNNF: {compile_res.getNbEdges()}")

# Get the compiled NNF circuit string (in standard d-DNNF format)
nnf_str = compile_res.getNNFString()
print("NNF String:\n", nnf_str)

2.3 Querying the Compiled d-DNNF

Once compiled, you can run multiple queries (SAT checks or model counting) under different literal assumptions:

# Check if the formula is satisfiable (no assumptions)
is_sat = compile_res.isSAT([])  # True/False

# Check satisfiability assuming x1 is True (1) and x2 is False (-2)
is_sat_under_assumptions = compile_res.isSAT([1, -2])

# Count models under literal assumptions
# E.g., model count assuming x1 is True
count_under_x1 = compile_res.count([1])
print(f"Models satisfying x1: {count_under_x1}")

2.4 Weighted Model Counting (WMC)

You can assign weights to literals for exact weighted model counting:

import py_d4

# Formula: (x1 or x2)
solver = py_d4.Solver([[1, 2]], nb_vars=2)

# Define weights for literals (keys are 1-based literals, values are string representations)
weights = {
    1: "0.3",
    -1: "0.7",
    2: "0.4",
    -2: "0.6"
}
# Set weights (WeightType can be FLOAT or GMP)
solver.setWeights(weights, py_d4.WeightType.FLOAT)

# Compute WMC directly
count_res = solver.count()
print("WMC Result:", float(count_res.getResult()))  # Output: 0.58

# Or compile and query WMC under assumptions
compile_res = solver.compile()
print("WMC under x1=True:", float(compile_res.count([1])))  # Output: 0.3

2.5 Logic Gates / Circuit Compilation

Instead of CNF, you can initialize the solver with logic gates to compile or count structured circuits:

import py_d4

# Create a gate representing: x3 = x1 AND (not x2)
gate = py_d4.Gate()
gate.gateType = py_d4.GateType.AND
gate.inputs = [1, -2]
gate.output = 3

# Instantiate solver from gate specifications
solver = py_d4.Solver([gate], nb_vars=3)
print("Models for circuit:", solver.count().getIntResult())

2.6 Solver Configuration & Options

Fine-tune the behavior of D4 by mutating native C++ option structures. Documentation and description of settings are exposed natively as Python docstrings:

import py_d4

# Instantiate default options
opt = py_d4.OptionDpllStyleMethod()

# 1. Read Option Descriptions (C++ docstrings exposed to Python)
print(py_d4.OptionDpllStyleMethod.exploitModel.__doc__)
# Output: "If we exploit model during search"

# 2. Modify properties directly (with type safety)
opt.precision = 30
opt.exploitModel = False
opt.optionSolver.solverName = 0  # 0: glucose, 1: minisat

# 3. Modify nested option group settings
opt.optionBranchingHeuristic.freqDecay = 98

# 4. Pass options to the Solver
solver = py_d4.Solver("formula.cnf", opt)

# 5. Serialize options to/from standard Python Dictionaries
config_dict = py_d4.dump_options_to_dict(opt)
opt_restored = py_d4.load_options_from_dict(config_dict)

# 6. Serialize options to/from raw JSON Strings (via native C++ bindings)
json_str = py_d4._py_d4.dump_options_to_json(opt)
opt_restored_json = py_d4._py_d4.load_options_from_json(json_str)

---

🛠️ Developers Guide

1. Requirements

Before building locally, ensure the following system-level dependencies are installed on your host:

• C++20 compatible compiler (e.g. GCC >= 10, Clang >= 10)
• CMake (>= 3.15)
• GMP development headers (libgmp-dev / gmp-devel)
• Zlib development headers (zlib1g-dev / zlib-devel)

2. Local Build Pipeline

To compile the C++ extension module and deploy it directly inside your local Python package tree, run:

# 1. Provide your GitLab access token to clone the D4 dependency
export GITLAB_TOKEN_LOGICAL="your_gitlab_token"

# 2. Configure, generate bindings, compile, and deploy shared library
./build.sh

Alternatively, you can install the package in editable mode via pip:

pip install -e .

3. Re-Generating Bindings

If D4 option headers change, you can automatically parse the new C++ classes and inline constructor descriptions to rebuild the nanobind bindings:

python3 scripts/generate_bindings.py /path/to/local/d4

(If /path/to/local/d4 is omitted, the script automatically searches the CMake FetchContent directory).

4. Running Tests

To execute the test suite and verify the integrity of the wrapper:

LD_PRELOAD=$(gcc -print-file-name=libstdc++.so.6) PYTHONPATH=. python3 tests/test_options.py

5. GitLab CI/CD Pipeline

The project includes an automated multi-stage .gitlab-ci.yml pipeline:

• Build Stage: Uses cibuildwheel to compile optimized, standalone Linux wheels for Python 3.8 to 3.13. It automatically routes the group-level GITLAB_TOKEN_LOGICAL CI variable to authenticate both the py-d4 and internal d4/optree sub-project checkouts.
• Deploy Stage: Triggered on pushing Git tags. Automatically publishes the generated wheel packages directly to the GitLab project PyPI package registry using twine.