There are prebuilt binaries available for each commit and release. These binaries are bundled with their dependencies. For details, see the README inside the release folder.
On (Linux) systems with an older glibc, the normal variant might not work. In this case, there is also the portable variant which is a self-extracting archive with everything bundled in one binary.
This project can be used and developed via a Nix flake.
With Nix installed simply run the following for a build:
nix build
The result will be at result.
To build without the need to clone the repository, use:
nix build github:SoftVarE-Group/d4v2
There is also a container image for usage with Docker, Podman or any other container tool.
For an overview, see here.
There is a tag for each branch and for each tagged release. To pull the container, use:
docker pull ghcr.io/softvare-group/d4v2
Then, you can use it like the standalone binary.
For d4 to be able to access files, you need to create a volume.
The following mounts <local/directory> on /work inside the container:
docker run -v <local/directory>:/work d4v2 --input /work/input.cnf --method ddnnf-compiler --dump-ddnnf /work/output.ddnnf
- CMake
- GMP (with C++ bindings)
- Boost (headers and
program_options) - zlib (optional, for glucose)
- Mt-KaHyPar
This is a CMake project.
To configure a debug build in the build directory (will be created), run:
cmake -B build
A generator can be specified, for example Ninja:
cmake -B build -G Ninja
Optionally, CMake variables can be set to alter the build:
cmake -D <variable>=<value> -D <variable>=<value> -B build
Of interest for this project are:
| Variable | Value | Description |
|---|---|---|
CMAKE_BUILD_TYPE |
Debug, Release, RelWithDebInfo or MinSizeRel |
Whether to create a debug or release build. |
D4_SOLVER |
minisat or glucose |
Which SAT solver to use. Defaults to minisat. |
D4_PREPROC_SOLVER |
minisat or glucose |
Which SAT solver to use for preprocessing. Defaults to minisat. |
CMAKE_INSTALL_PREFIX |
Path | Where to install built files to using cmake --install. |
MtKaHyPar_ROOT |
Path | Alternative root directory so search for Mt-KaHyPar. |
glucose_ROOT |
Path | Alternative root directory so search for glucose. |
After configuring, build the project with:
cmake --build build
The resulting executable will be built at build/d4.
To install the built files, use:
cmake --install build
The installation prefix can be changed as described in the build section.
See the help message:
d4 --help
To compile a CNF into a d-DNNF, use:
d4 --input /path/to/input.cnf --method ddnnf-compiler --dump-ddnnf /path/to/output.ddnnf