3.1.5. cnfformula.families.pebbling module¶
Implementation of the pigeonhole principle formulas
-
class
PebblingCmdHelper
¶ 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.
-
static
-
PebblingFormula
(digraph)¶ Pebbling formula
Build a pebbling formula from the directed graph. If the graph has an ordered_vertices attribute, then it is used to enumerate the vertices (and the corresponding variables).
Arguments: - digraph: directed acyclic graph.
-
class
SparseStoneCmdHelper
¶ Sparse Stone formulas
This is a variant of the
StoneFormula()
. See that for a description of the formula. This variant is such that each vertex has only a small selection of which stone can go to that vertex. In particular which stones are allowed on each vertex is specified by a bipartite graph \(B\) on which the left vertices represent the vertices of DAG \(D\) and the right vertices are the stones.If a vertex of \(D\) correspond to the left vertex \(v\) in \(B\), then its neighbors describe which stones are allowed for it.
The vertices in \(D\) do not need to have the same name as the one on the left side of \(B\). It is only important that the number of vertices in \(D\) is the same as the vertices in the left side of \(B\).
In that case the element at position \(i\) in the ordered sequence
enumerate_vertices(D)
corresponds to the element of rank \(i\) in the sequence of left side vertices of \(B\) according to the output ofLeft, Right = bipartite_sets(B)
.Standard
StoneFormula()
is essentially equivalent to a sparse stone formula where \(B\) is the complete graph.Parameters: - D : a directed acyclic graph
it should be a directed acyclic graph.
- B : bipartite graph
Raises: - ValueError
if \(D\) is not a directed acyclic graph
- ValueError
if \(B\) is not a bipartite graph
- ValueError
when size differs between \(D\) and the left side of \(B\)
See also
Methods
build_cnf
(args)Build the pebbling formula setup_command_line
(parser)Setup the command line options for stone formulas -
static
build_cnf
(args)¶ Build the pebbling formula
Arguments: - args: command line options
-
description
= 'stone formula (sparse version)'¶
-
name
= 'stonesparse'¶
-
static
setup_command_line
(parser)¶ Setup the command line options for stone formulas
Arguments: - parser: parser to load with options.
-
SparseStoneFormula
(D, B)¶ Sparse Stone formulas
This is a variant of the
StoneFormula()
. See that for a description of the formula. This variant is such that each vertex has only a small selection of which stone can go to that vertex. In particular which stones are allowed on each vertex is specified by a bipartite graph \(B\) on which the left vertices represent the vertices of DAG \(D\) and the right vertices are the stones.If a vertex of \(D\) correspond to the left vertex \(v\) in \(B\), then its neighbors describe which stones are allowed for it.
The vertices in \(D\) do not need to have the same name as the one on the left side of \(B\). It is only important that the number of vertices in \(D\) is the same as the vertices in the left side of \(B\).
In that case the element at position \(i\) in the ordered sequence
enumerate_vertices(D)
corresponds to the element of rank \(i\) in the sequence of left side vertices of \(B\) according to the output ofLeft, Right = bipartite_sets(B)
.Standard
StoneFormula()
is essentially equivalent to a sparse stone formula where \(B\) is the complete graph.Parameters: - D : a directed acyclic graph
it should be a directed acyclic graph.
- B : bipartite graph
Raises: - ValueError
if \(D\) is not a directed acyclic graph
- ValueError
if \(B\) is not a bipartite graph
- ValueError
when size differs between \(D\) and the left side of \(B\)
See also
-
class
StoneCmdHelper
¶ 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.
Note
The exact formula structure depends by the graph and on its topological order, which is determined by the
enumerate_vertices(D)
.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, 3) M. Alekhnovich, J. Johannsen, T. Pitassi and A. Urquhart An Exponential Separation between Regular and General Resolution. Theory of Computing (2007) [2] (1, 2) R. Raz and P. McKenzie Separation of the monotone NC hierarchy. Combinatorica (1999) Methods
build_cnf
(args)Build the pebbling formula setup_command_line
(parser)Setup the command line options for stone formulas -
static
build_cnf
(args)¶ Build the pebbling formula
Arguments: - args: command line options
-
description
= 'stone formula'¶
-
name
= 'stone'¶
-
static
setup_command_line
(parser)¶ Setup the command line options for stone formulas
Arguments: - parser: parser to load with options.
-
StoneFormula
(D, nstones)¶ 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.
Note
The exact formula structure depends by the graph and on its topological order, which is determined by the
enumerate_vertices(D)
.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, 3) M. Alekhnovich, J. Johannsen, T. Pitassi and A. Urquhart An Exponential Separation between Regular and General Resolution. Theory of Computing (2007) [2] (1, 2) R. Raz and P. McKenzie Separation of the monotone NC hierarchy. Combinatorica (1999)
-
stone_formula_helper
(F, D, mapping)¶ Stones formulas helper
Builds the clauses of a stone formula given the mapping object between stones and vertices of the DAG. THis is not supposed to be called by user code, and indeed this function assumes the following facts.
- \(D\) is equal to mapping.domain()
- \(D\) is a DAG
Parameters: - F : CNF
the CNF which will contain the clauses of the stone formula
- D : a directed acyclic graph
it should be a directed acyclic graph.
- mapping : unary_mapping object
mapping between stones and graph vertices
See also
StoneFormula
- the classic stone formula
SparseStoneFormula
- stone formula with sparse mapping