dimacs_cnf.h File Reference

Parse a DIMACS CNF into a ProvSQL BooleanCircuit. More...

#include <string>
#include "BooleanCircuit.h"

Include dependency graph for dimacs_cnf.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
gate_t	parse_dimacs_cnf (const std::string &text, BooleanCircuit &c, bool weighted)
	Parse text (a DIMACS CNF) into c and return the root gate.

Detailed Description

Parse a DIMACS CNF into a ProvSQL BooleanCircuit.

Reads the "p cnf" header, the clause lines, and the Model Counting Competition weight lines ("c p weight <lit> <w> 0"). Builds an AND-of-OR-of-literal Boolean circuit: one IN gate per variable, a shared NOT per negated variable, an OR per clause, and an AND root.

For weighted model counting (weighted) each input gate's probability is set to the weight of its positive literal, defaulting to 0.5 when no weight is given; ProvSQL's evaluator then takes the complementary weight 1-p for the negative literal (the probability model the "c p weight" lines ProvSQL itself emits already satisfy). Used by the tdkc KCMCP server.

Definition in file dimacs_cnf.h.

Function Documentation

parse_dimacs_cnf()

gate_t parse_dimacs_cnf	(	const std::string &	text,
		BooleanCircuit &	c,
		bool	weighted )

Parse text (a DIMACS CNF) into c and return the root gate.

Exceptions

std::runtime_error

on a malformed input.

Definition at line 33 of file dimacs_cnf.cpp.

Here is the call graph for this function: