Crate tididi_cnf

Crate tididi_cnf 

Source
Expand description

A knowledge compiler and model counter for CNF.

tididi-cnf compiles a DIMACS CNF formula into a Tree Decision Diagram (TDD), a canonical circuit that holds all of the formula’s models, which the [tididi] library saves, combines with other circuits and queries as evidence or weights change. The same compiler is a model counter: it answers the model count, the weighted model count and their projections onto a set of variables, the model count and the projected counts exactly, the weighted model count in a bounded-precision log domain. It preprocesses the formula, chooses a vtree for what is left and compiles it bottom-up, with fallbacks when a compile runs out of time or memory. It is the library behind the tididi binary, and count makes the binary’s whole run on one instance.

§Compile a formula

count takes an instance, the task, and the Limits to run under, and returns an Answer: the verdict, the Count, the run’s Stats and, for a compile, the diagram. Here the instance is the eight queens puzzle, read from a DIMACS file whose variable 1 is a corner square, and the compiled circuit then counts the placements with a queen there without compiling again:

use tididi_cnf::tididi::Literal;
use tididi_cnf::{count, Limits, Mode};

let answer = count("tests/data/queens8.cnf", Some(Mode::Compile), &Limits::default())?;
let board = answer.diagram().expect("a compile keeps its circuit");
println!("Placements: {}", board.model_count()?);
let mut counter = board.counter()?;
counter.observe([Literal::try_from(1)?])?;
println!("With a queen in a corner: {}", counter.model_count()?);

Output:

Placements: 92
With a queen in a corner: 4

§Count its models

A counting task returns the count without keeping a circuit. Here the instance is (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3), parsed from DIMACS text with parse_dimacs, and the task is its model count:

use tididi_cnf::{count, parse_dimacs, Limits, Mode};

let formula = parse_dimacs("p cnf 3 3\n1 2 0\n-1 3 0\n-2 -3 0\n".as_bytes())?;
let answer = count(formula, Some(Mode::Mc), &Limits::default())?;
println!("Models: {}", answer.count());

Output:

Models: 2

With None for the mode, the instance’s header chooses the task, as it does for the binary.

A program that builds its formula holds it as data rather than text: formula_from_clauses takes the clauses as DIMACS integers, with a show set and literal weights for the tasks that read them, and returns what parse_dimacs returns for the same formula.

use tididi_cnf::{count, formula_from_clauses, Limits, Mode};

let formula = formula_from_clauses(3, [[1, 2], [-1, 3], [-2, -3]], None, &[])?;
let answer = count(formula, Some(Mode::Mc), &Limits::default())?;
println!("Models: {}", answer.count());

Output:

Models: 2

§Tasks and input

The instance is DIMACS CNF. Its c t mc|wmc|pmc|pwmc line names the task (Mode): the model count, the weighted count, and their projected forms, with c p weight lines for the literal weights and a c p show line for the variables projected onto; a formula that declares neither a task nor a show set is compiled. The user guide describes the input format, the answers and the binary.

§One step at a time

Below count are the steps a compile is made of, for a caller that wants the diagram and its own choices at each: parse_dimacs reads the formula, vtree::build_vtree builds a vtree for it from a spec with its vtree::VtreeOptions, and compile::compile_cnf compiles it on that vtree under its compile::CompileOptions into a [tididi::Tdd], the diagram of what it returns, whose queries the [tididi] crate provides. This path runs no preprocessing and no fallback.

use std::fs::File;
use std::io::BufReader;

use tididi_cnf::compile::{compile_cnf, CompileOptions};
use tididi_cnf::vtree::{build_vtree, VtreeOptions};

// Five queens on a 5×5 board, none attacking another.
let file = BufReader::new(File::open("tests/data/queens5.cnf")?);
let (formula, _header) = tididi_cnf::parse_dimacs(file)?;
let vtree = build_vtree(&formula, "portfolio", &VtreeOptions::default())?;
let diagram = vtree
    .context()
    .run(|engine| compile_cnf(engine, &formula, &vtree, CompileOptions::default()))?
    .diagram;
println!("{} placements", diagram.model_count()?);

Output:

10 placements

§Applications

The configuration example counts a product’s configurations, projects them onto some of the options, and queries the compiled rules as a customer chooses. The reliability example weighs links by their probabilities to find how likely two sites stay connected. The circuit example counts the distinct products a multiplier outputs. The vtree example compiles one formula on several vtrees and compares the circuits.

The guide holds these worked examples and the architecture reference.

§Limits

Limits are the binary’s --time-limit-ms and --mem-limit-mb. The time limit bounds the whole run: every stage gets a share of it, and a run that reaches it returns Error::Incomplete, never a partial count. The memory limit lowers the process’s address-space limit while the run lasts, and a model count that is refused memory retries on smaller pieces of the formula; the call puts the limit back when it returns. The default sets neither. A run that nears the address-space limit switches the allocator to handing freed pages back to the system at once, and the process keeps that setting after the run returns.

Calls from several threads run one at a time: a count call waits for the one in progress to return. count prints its progress to stderr, as the binary does.

§Platform

Linux, and WebAssembly through Emscripten (wasm32-unknown-emscripten). Preprocessing and vtree construction come from the vitri crate, which builds CaDiCaL, Arjun and their dependencies from source and links them natively; its building guide lists the C++ toolchain it needs, for either target. Natively the crate installs jemalloc as the global allocator, so a program that links it cannot choose its own, and it exports jemalloc’s startup configuration, which then holds for the whole process. Recovering from a refused allocation needs panic = "unwind", the default. WebAssembly keeps the target’s own allocator and has no address-space limit to lower, so it refuses Limits::mem_limit_mb.

§Module reference

Re-exports§

pub use tididi;
pub use vitri;

Modules§

compile
The compiler: a CNF formula and a vtree in, a Tree Decision Diagram out.
guide
The worked examples put the crate to work on applications, from counting a product’s configurations to the distinct outputs of a circuit. Using diagrams from the compiler runs a bounded compile from Rust and queries its diagram. The architecture reference maps the source for contributors. The binary, the input format and the run record are in the command-line guide.
vtree
Vtree construction for the compiler, and the descriptors of a formula’s independent components.

Structs§

Answer
What a run answered: the mode it ran, whether the formula has a model, the count, and the run’s record.
Limits
The limits a run works under: the time it may take and the address space it may use.
Stats
One run, as a harness or a researcher reads it back: the record the binary’s --stats writes, as a value.

Enums§

Count
A count, in the domain its task produces.
Error
Everything that stops a run before it has an answer.
Input
The instance a run reads: a DIMACS file, or a formula already parsed with its header.
Mode
What a run answers: one of the four counting tasks, or a compile.

Functions§

count
Count, or compile, one instance: the task mode names, or the one its header declares, under limits.
formula_from_clauses
Build a formula from clauses of DIMACS integers, with the header lines a projected or weighted count reads.
parse_dimacs
Read DIMACS text into a formula and the header lines that came with it.