cnfgen.clihelpers.pebbling_helpers module¶

Implementation of some graph formulas helpers

class PebblingCmdHelper¶

Bases: cnfgen.clihelpers.formula_helpers.FormulaHelper

Command line helper for pebbling formulas

Methods

`build_cnf`(args)	Build the pebbling formula
`setup_command_line`(parser)	Setup the command line options for pebbling formulas

static build_cnf(args)¶

Build the pebbling formula

Arguments: - args: command line options

description = 'pebbling formula'¶

name = 'peb'¶

static setup_command_line(parser)¶

Setup the command line options for pebbling formulas

Arguments: - parser: parser to load with options.

class StoneCmdHelper¶

Bases: cnfgen.clihelpers.formula_helpers.FormulaHelper

Stone formulas

The stone formulas have been introduced in [2] and generalized in [1]. They are one of the classic examples that separate regular resolutions from general resolution [1].

A “Stones formula” from a directed acyclic graph \(D\) claims that each vertex of the graph is associated with one on \(s\) stones (not necessarily in an injective way). In particular for each vertex \(v\) in \(V(D)\) and each stone \(j\) we have a variable \(P_{v,j}\) that claims that stone \(j\) is associated to vertex \(v\).

Each stone can be either red or blue, and not both. The propositional variable \(R_j\) if true when the stone \(j\) is red and false otherwise.

The clauses of the formula encode the following constraints. If a stone is on a source vertex (i.e. a vertex with no incoming edges), then it must be red. If all stones on the predecessors of a vertex are red, then the stone of the vertex itself must be red.

The formula furthermore enforces that the stones on the sinks (i.e. vertices with no outgoing edges) are blue.

Parameters:	D : a directed acyclic graph it should be a directed acyclic graph. nstones : int the number of stones.
Raises:	ValueError if \(D\) is not a directed acyclic graph ValueError if the number of stones is negative

References

[1]	(1, 2) M. Alekhnovich, J. Johannsen, T. Pitassi and A. Urquhart An Exponential Separation between Regular and General Resolution. Theory of Computing (2007)

[2]	R. Raz and P. McKenzie Separation of the monotone NC hierarchy. Combinatorica (1999)

Methods

`build_cnf`(args)	Build the stone formula
`setup_command_line`(parser)	Setup the command line options for stone formulas

static build_cnf(args)¶

Build the stone formula

Arguments: - args: command line options

description = 'stone formula (dense and sparse)'¶

name = 'stone'¶

static setup_command_line(parser)¶

Setup the command line options for stone formulas

Arguments: - parser: parser to load with options.