cnfgen.formula.mapping module¶

CNF encoding of mapping

The module defines functionality to conviniently represent mapping, - in unary encoding - in binary encoding - in sparse unary encoding

The module implements the CNFMapping object, which is supposed to be inherited from the VariablesManager object.

class BinaryMappingVariables(formula, n, m, labelfmt='v({}, {})')¶

Bases: cnfgen.formula.variables.BaseVariableGroup

A group of variables representing a mapping to bitstrings

Given a domain \([n]\) and a range \([m]\), this group of variables represent a mapping.

Variables are \(v(i,k-1)...v(i,0)\) for \(i \in D\). Each \(v(i,k-1)...v(i,0)\) is a string of \(k\) bits, and represents the image of \(i \in [m]\). The value \(k\) is set so that

Methods

`__call__`(*index)	Convert the index of a variable into its ID.
`domain`()	The domain of the mapping
`forbid`(i, j)	The clause that forbids i–>j
`indices`(*pattern)	Implementation of :py:classmethod:`BaseVariableGroup.indices`
`label`(*pattern)	Convert the index of a variable into its label.
`parent_formula`()	The formula associated to the variable group
`range`()	The range of the mapping
`to_index`(lit)	Convert a literal to the corresponding pair (i,b)

bits
to_dict

bits()¶

domain()¶

The domain of the mapping

If v is None it returns the domain of the mapping. Otherwise it returns the sequence of elements which is possible to map to v.

Examples

>>> F = CNFMapping()
>>> f = BinaryMappingVariables(F,4,6)
>>> f.domain() == range(1,5)
True
>>> F = CNFMapping()
>>> f = BinaryMappingVariables(F,20,6)
>>> f.domain() == range(1,21)
True

forbid(i, j)¶

The clause that forbids i–>j

Create the unique clause that is false if and only if i is mapped to the bit string corresponding to j

Examples

>>> F = CNFMapping()
>>> V = BinaryMappingVariables(F,4,6)
>>> V.forbid(2,0)
[4, 5, 6]
>>> V.forbid(2,7)
[-4, -5, -6]
>>> V.forbid(4,3)
[10, -11, -12]

indices(*pattern)¶

Implementation of :py:classmethod:`BaseVariableGroup.indices`

Parameters:	pattern : sequences(positive integers or None) the pattern of the indices
Returns:	a tuple or an itertools.product object

Examples

>>> F = CNFMapping()
>>> f = BinaryMappingVariables(F,5,12)
>>> print(*f.indices(3,None))
(3, 3) (3, 2) (3, 1) (3, 0)
>>> print(*f.indices(None,1))
(1, 1) (2, 1) (3, 1) (4, 1) (5, 1)

range()¶

The range of the mapping

If u is None it returns the range of the mapping. Otherwise it returns the sequence of all elements to which u can be mapped.

Examples

>>> F = CNFMapping()
>>> f = BinaryMappingVariables(F,5,12)
>>> f.range() == range(0,12)
True
>>> len(f)
20
>>> F = CNFMapping()
>>> f = BinaryMappingVariables(F,5,15)
>>> f.range() == range(0,15)
True
>>> len(f)
20

to_index(lit)¶

Convert a literal to the corresponding pair (i,b)

Parameters:	lit : positive or negative literal -ID or +ID for the ID of the variable
Returns:	pair of integers
Raises:	ValueError when lit is not within the appropriate intervals

Examples

>>> F = CNFMapping()
>>> F.update_variable_number(10)
>>> V = BinaryMappingVariables(F,10, 13, labelfmt='v({},{})')
>>> len(V)
40
>>> V.to_index(11)
(1, 3)
>>> V.to_index(16)
(2, 2)
>>> V.to_index(-18)
(2, 0)
>>> V.to_index(48)
(10, 2)

class CNFMapping(clauses=None, description=None)¶

Bases: cnfgen.formula.variables.VariablesManager

CNF with a variable manager

A CNF formula needs to keep track on variables. A VariableManager allows to do that, while providing a nice interface that allows to focus on variable meaning.

Examples

>>> F=CNFMapping()
>>> f = F.new_mapping(2,3,label='f_{{{},{}}}')
>>> F.number_of_variables()
6
>>> B = BipartiteGraph(4,4)
>>> B.add_edges_from([(1,2), (1,4), (2,3), (4,2), (4,3)])
>>> g = F.new_sparse_mapping(B, label='g_{{{},{}}}')
>>> F.number_of_variables()
11
>>> print(*f.label())
f_{1,1} f_{1,2} f_{1,3} f_{2,1} f_{2,2} f_{2,3}
>>> print(*g.label())
g_{1,2} g_{1,4} g_{2,3} g_{4,2} g_{4,3}

Attributes:	name : dict associate a variable / literal to its label

Methods

new_mapping(n, m, label):	add the variables representing a mapping (in unary)
new_sparse_mapping(B, label):	add the variables representing a sparse mapping

force_complete_mapping(f)¶

Enforce the mapping f to be complete

Add the clauses that make the mapping f complete. Namely that all elements in the domain are mapped to some element in the range. These clauses do not exclude the possibility that an element from the domain is mapped to multiple elements in the range (indeed that may be the case for unary representation).

(See py:classmethod:CNFMapping.force_functional_mapping)

Examples

>>> C = CNFMapping()
>>> f = C.new_mapping(10,5)
>>> C.force_complete_mapping(f)
>>> C[2]
[11, 12, 13, 14, 15]
>>> len(C)
10
>>> g = C.new_binary_mapping(4,14)
>>> C.force_complete_mapping(g)
>>> len(C)
18
>>> C[10]
[-51, -52, -53, 54]
>>> C[11]
[-51, -52, -53, -54]

force_functional_mapping(f)¶

Enforce the mapping f to be functional

Add the clauses that enforce the mapping f to be a partial function. Namely that every element in the domain can be mapped to at most one element in the range.

Together with :py:classmethod:`CNFMapping.force_complete_mapping`, this enforces the mapping to be a total function.

Examples

>>> C = CNFMapping()
>>> f = C.new_mapping(10,5)
>>> C.force_functional_mapping(f)
>>> len(C)
100
>>> C.number_of_variables()
50
>>> max(len(cls) for cls in C)
2
>>> C[7]
[-3, -4]
>>> len(C)
100

force_injective_mapping(f)¶

Enforce the mapping f to be injective

Add the clauses that make the mapping f injective. Namely that all elements in the range have at most one element in the domain mapped to it.

Examples

>>> C = CNFMapping()
>>> f = C.new_mapping(10,5)
>>> C.force_injective_mapping(f)
>>> C[0]
[-1, -6]
>>> C[1]
[-1, -11]
>>> C[45]
[-2, -7]
>>> len(C)
225

force_nondecreasing_mapping(f)¶

Enforce the mapping f to be non decreasing

Add the clauses that make the mapping f injective. Namely that all elements in the range have at most one element in the domain mapped to it.

Examples

>>> C = CNFMapping()
>>> B = BipartiteGraph(2,3)
>>> B.add_edge(1,2)
>>> B.add_edge(1,3)
>>> B.add_edge(2,1)
>>> B.add_edge(2,3)
>>> f = C.new_sparse_mapping(B)
>>> C.force_nondecreasing_mapping(f)
>>> len(C)
2
>>> C[0]
[-1, -3]
>>> C[1]
[-2, -3]
>>> g = C.new_binary_mapping(2,4)
>>> C.force_nondecreasing_mapping(g)
>>> len(C)
8

force_surjective_mapping(f)¶

Enforce the mapping f to be surjective

Add the clauses that make the mapping f surjective. Namely that all elements in the range have at least one element in the domain mapped to it.

This method works only for mapping represented in unary.

Examples

>>> C = CNFMapping()
>>> f = C.new_mapping(10,5)
>>> C.force_surjective_mapping(f)
>>> C[1]
[2, 7, 12, 17, 22, 27, 32, 37, 42, 47]
>>> len(C)
5

new_binary_mapping(n, m, label='v({}, {})')¶

Adds variables for a mapping from n to m encoded in binary

Creates a group of variables representing a mapping from \(\{1,\ldots,n}\) to \(\{0,\ldots,m-1\}\).

The mapping is represented as a sequence of \(n\) binary strings of length \(k\), where \(k\) is the smallest integer so that \(m \leq 2^k\).

The element mapped to \(i\) is represented using \(k\) boolean variables \(v(i,k-1) \ldots v(i,0)\).

Parameters:	n : int size of the domain m : int size of the range label : str, optional string representation of the variables
Returns:	BinaryMappingVariables, the new variable group

Examples

>>> F = CNFMapping()
>>> f = F.new_binary_mapping(4,14)
>>> F.number_of_variables()
16
>>> f(2,3)
5
>>> f(4,0)
16

new_mapping(n, m, label='f({})={}')¶

Adds variables for a mapping from n to m

Creates a group of variables for a mapping from \(n\) elements to \(m\) elements represented as boolean variables \(f_{i,j}\) for \(i in [n]\) and \(j in [m]\).

Parameters:	n : int size of the domain m : int size of the range label : str, optional string representation of the variables
Returns:	UnaryMappingVariables, the new variable group

Examples

>>> F = CNFMapping()
>>> f = F.new_mapping(4,10)
>>> f(2,1)
11
>>> f(1,8)
8
>>> F.number_of_variables()
40
>>> f.label(3,8)
'f(3)=8'

new_sparse_mapping(B, label='f({})={}')¶

Adds variables for a sparse mapping

Creates a group of variables representing a mapping. The representation is sparse in the sense that the domain and range are the two sides of a bipartite graph \(B\). The map \(u \mapsto v\) is available if and only if the edge \((u,v) \in E(B)\).

Parameters:	B : BipartiteGraph sparse representation of the mapping label : str, optional string representation of the variables
Returns:	UnaryMappingVariables, the new variable group

Examples

>>> B = BipartiteGraph(5,3)
>>> B.add_edge(2,1)
>>> B.add_edge(1,3)
>>> B.add_edge(2,2)
>>> B.add_edge(3,3)
>>> B.add_edge(4,3)
>>> B.add_edge(4,2)
>>> B.add_edge(5,1)
>>> F = CNFMapping()
>>> f = F.new_sparse_mapping(B)
>>> f(2,2)
3
>>> f(4,3)
6
>>> F.number_of_variables()
7
>>> f.label(4,2)
'f(4)=2'

class UnaryMappingVariables(formula, G, labelfmt)¶

Bases: cnfgen.formula.variables.BipartiteEdgesVariables

A group of variables representing a mapping

The mapping is represented in unary, where variables \(f_{i,j}\) represent atoms \(f(i)=j\).

Assuming \(i \in D\) and \(j \in R\), to all pairs \(D \times R\) are necessarily available. The ones that are possible are specified by a bipartite graph \(G=(D,R,E)\).

Methods

`__call__`(*index)	Convert the index of a variable into its ID.
`domain`([v])	The domain of the mapping
`indices`(*pattern)	Print the label of the edge
`label`(*pattern)	Convert the index of a variable into its label.
`parent_formula`()	The formula associated to the variable group
`range`([u])	The range of the mapping
`to_index`(lit)	Convert a literal to the corresponding edge

to_dict

domain(v=None)¶

The domain of the mapping

If v is None it returns the domain of the mapping. Otherwise it returns the sequence of elements which is possible to map to v.

range(u=None)¶

The range of the mapping

If u is None it returns the range of the mapping. Otherwise it returns the sequence of all elements to which u can be mapped.