Module reference¶
Module contents¶
-
class
nnf.
NNF
[source]¶ Bases:
object
Base class for all NNF sentences.
-
clause
() → bool[source]¶ The sentence is a clause.
Clauses are Or nodes with variable children that don’t share names.
-
consistent
() → bool¶ Some set of values exists that makes the sentence correct.
This method doesn’t necessarily try to find an example, which can make it faster. It’s decent at decomposable sentences and sentences in CNF, and bad at other sentences.
-
contradicts
(other: nnf.NNF) → bool[source]¶ There is no set of values that satisfies both sentences.
-
deduplicate
() → T_NNF[source]¶ Return a copy of the sentence without any duplicate objects.
If a node has multiple parents, it’s possible for it to be represented by two separate objects. This method gets rid of that duplication.
It’s better to avoid the duplication in the first place. This method is for diagnostic purposes, in combination with
object_count()
.
-
deterministic
() → bool[source]¶ The children of each Or node contradict each other.
May be very expensive.
-
entails
(other: nnf.NNF) → bool¶ Return whether
other
is always true if the sentence is true.This is faster if
self
is a term orother
is a clause.
-
equivalent
(other: nnf.NNF) → bool[source]¶ Test whether two sentences have the same models.
If the sentences don’t contain the same variables they are considered equivalent if the variables that aren’t shared are independent, i.e. their value doesn’t affect the value of the sentence.
-
flat
() → bool[source]¶ A sentence is flat if its height is at most 2.
That is, there are at most two layers below the root node.
-
forget
(names: Iterable[Hashable]) → nnf.NNF[source]¶ Forget a set of variables from the theory.
Has the effect of returning a theory without the variables provided, such that every model of the new theory has an extension (i.e., an assignment) to the forgotten variables that is a model of the original theory.
Parameters: names – An iterable of the variable names to be forgotten
-
implicants
() → nnf.Or[nnf.And[nnf.Var]][nnf.And[nnf.Var][nnf.Var]][source]¶ Extract the prime implicants of the sentence.
Prime implicants are the minimal terms that imply the sentence. This method returns a disjunction of terms that’s equivalent to the original sentence, and minimal, meaning that there are no terms that imply the sentence that are strict subsets of any of the terms in this representation, so no terms could be made smaller.
-
implicates
() → nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]][source]¶ Extract a prime implicate cover of the sentence.
Prime implicates are the minimal implied clauses. This method returns a conjunction of clauses that’s equivalent to the original sentence, and minimal, meaning that there are no clauses implied by the sentence that are strict subsets of any of the clauses in this representation, so no clauses could be made smaller.
While
implicants()
returns all implicants, this method may only return some of the implicates.
-
implies
(other: nnf.NNF) → bool[source]¶ Return whether
other
is always true if the sentence is true.This is faster if
self
is a term orother
is a clause.
-
is_CNF
(strict: bool = False) → bool[source]¶ Return whether the sentence is in the Conjunctive Normal Form.
Parameters: strict – If True
, follow the definition of the Knowledge Compilation Map, requiring that a variable doesn’t appear multiple times in a single clause.
-
is_DNF
(strict: bool = False) → bool[source]¶ Return whether the sentence is in the Disjunctive Normal Form.
Parameters: strict – If
True
, follow the definition of the Knowledge Compilation Map, requiring that a variable doesn’t appear multiple times in a single term.
-
is_MODS
() → bool[source]¶ Return whether the sentence is in MODS form.
MODS sentences are disjunctions of terms representing models, making the models trivial to enumerate.
-
leaf
() → bool[source]¶ True if the node doesn’t have children.
That is, if the node is a variable, or one of
true
andfalse
.
-
make_pairwise
() → nnf.NNF[source]¶ Alter the sentence so that all internal nodes have two children.
This can be easier to handle in some cases.
-
mark_deterministic
() → None[source]¶ Declare for optimization that this sentence is deterministic.
Note that this goes by object identity, not equality. This may matter in obscure cases where you instantiate the same sentence multiple times.
-
model_count
() → int[source]¶ Return the number of models the sentence has.
This can be done efficiently for sentences that are decomposable and deterministic.
-
models
() → Iterator[Dict[Hashable, bool]][source]¶ Yield all dictionaries of values that make the sentence correct.
Much faster on sentences that are decomposable. Even faster if they’re also deterministic.
-
project
(names: Iterable[Hashable]) → nnf.NNF[source]¶ Dual of
forget()
: will forget all variables not given
-
satisfiable
() → bool[source]¶ Some set of values exists that makes the sentence correct.
This method doesn’t necessarily try to find an example, which can make it faster. It’s decent at decomposable sentences and sentences in CNF, and bad at other sentences.
-
satisfied_by
(model: Dict[Hashable, bool]) → bool[source]¶ The given dictionary of values makes the sentence correct.
-
simplify
(merge_nodes: bool = True) → nnf.NNF[source]¶ Apply the following transformations to make the sentence simpler:
- If an And node has false as a child, replace it by false
- If an Or node has true as a child, replace it by true
- Remove children of And nodes that are true
- Remove children of Or nodes that are false
- If an And or Or node only has one child, replace it by that child
- If an And or Or node has a child of the same type, merge them
Parameters: merge_nodes – if False
, don’t merge internal nodes. In certain cases, merging them may increase the size of the sentence.
-
size
() → int[source]¶ The number of edges in the sentence.
Note that sentences are rooted DAGs, not trees. If a node has multiple parents its edges will still be counted just once.
-
solve
() → Optional[Dict[Hashable, bool]][source]¶ Return a satisfying model, or
None
if unsatisfiable.
-
term
() → bool[source]¶ The sentence is a term.
Terms are And nodes with variable children that don’t share names.
-
to_CNF
(simplify: bool = True) → nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]][source]¶ Compile theory to a semantically equivalent CNF formula.
Parameters: simplify – If True, simplify clauses even if that means eliminating variables.
-
to_DOT
(*, color: bool = False, color_dict: Optional[Dict[str, str]] = None, label: str = 'text', label_dict: Optional[Dict[str, str]] = None) → str[source]¶ Return a representation of the sentence in the DOT language.
DOT is a graph visualization language.
Parameters: - color – If
True
, color the nodes. This is a bit of an eyesore, but might make them easier to understand. - label – If
'text'
, the default, label nodes with “AND”, “OR”, etcetera. If'symbol'
, label them with unicode symbols like “∧” and “⊥”. - color_dict – Use an alternative palette. This should be a
dictionary with keys
'and'
,'or'
,'true'
,'false'
,'var'
and'neg'
. Not all keys have to be included. Passing a dictionary impliescolor=True
. - label_dict – Use alternative labels for nodes. This should be
a dictionary with keys
'and'
,'or'
,'true'
and'false'
. Not all keys have to be included.
- color – If
-
to_MODS
() → nnf.Or[nnf.And[nnf.Var]][nnf.And[nnf.Var][nnf.Var]][source]¶ Convert the sentence to a MODS sentence.
-
to_model
() → Dict[Hashable, bool][source]¶ If the sentence directly represents a model, convert it to that.
A sentence directly represents a model if it’s a conjunction of (unique) variables, or a single variable.
-
-
class
nnf.
Internal
(children: Iterable[T_NNF_co] = ())[source]¶ Bases:
nnf.NNF
,typing.Generic
Base class for internal nodes, i.e. And and Or nodes.
-
children
¶
-
-
class
nnf.
And
(children: Iterable[T_NNF_co] = ())[source]¶ Bases:
nnf.Internal
Conjunction nodes, which are only true if all of their children are.
-
class
nnf.
Or
(children: Iterable[T_NNF_co] = ())[source]¶ Bases:
nnf.Internal
Disjunction nodes, which are true if any of their children are.
-
class
nnf.
Var
(name: Hashable, true: bool = True)[source]¶ Bases:
nnf.NNF
A variable, or its negation.
If its name is a string, its repr will use that name directly. Otherwise it will use more ordinary constructor syntax.
>>> a = Var('a') >>> a a >>> ~a ~a >>> b = Var('b') >>> a | ~b == Or({Var('a', True), Var('b', False)}) True >>> Var(10) Var(10) >>> Var(('a', 'b'), False) ~Var(('a', 'b'))
-
name
¶
-
true
¶
-
-
class
nnf.
Aux
(hex=None, bytes=None, bytes_le=None, fields=None, int=None, version=None, *, is_safe=<SafeUUID.unknown: None>)[source]¶ Bases:
uuid.UUID
Unique UUID labels for auxiliary variables.
Don’t instantiate directly, call
Var.aux()
instead.
-
nnf.
all_models
(names: Iterable[Hashable]) → Iterator[Dict[Hashable, bool]][source]¶ Yield dictionaries with all possible boolean values for the names.
>>> list(all_models(["a", "b"])) [{'a': False, 'b': False}, {'a': False, 'b': True}, ...
-
nnf.
complete_models
(models: Iterable[Dict[Hashable, bool]], names: Iterable[Hashable]) → Iterator[Dict[Hashable, bool]][source]¶
-
nnf.
decision
(var: nnf.Var, if_true: T_NNF, if_false: U_NNF) → nnf.Or[typing.Union[nnf.And[typing.Union[nnf.Var, ~T_NNF]], nnf.And[typing.Union[nnf.Var, ~U_NNF]]]][Union[nnf.And[typing.Union[nnf.Var, ~T_NNF]][Union[nnf.Var, T_NNF]], nnf.And[typing.Union[nnf.Var, ~U_NNF]][Union[nnf.Var, U_NNF]]]][source]¶ Create a decision node with a variable and two branches.
Parameters: - var – The variable node to decide on.
- if_true – The branch if the decision is true.
- if_false – The branch if the decision is false.
-
nnf.
true
= true¶ A node that’s always true. Technically an And node without children.
-
nnf.
false
= false¶ A node that’s always false. Technically an Or node without children.
Submodules¶
nnf.operators module¶
Convenience functions for logical relationships that are not part of NNF.
These functions will simulate those relationships, often by doubling sentences or altering their structure to negate them. This makes them inefficient.
-
nnf.operators.
xor
(a: nnf.NNF, b: nnf.NNF) → nnf.Or[nnf.And[nnf.NNF]][nnf.And[nnf.NNF][nnf.NNF]][source]¶ Exactly one of the operands is true.
-
nnf.operators.
nand
(a: nnf.NNF, b: nnf.NNF) → nnf.Or[nnf.NNF][nnf.NNF][source]¶ At least one of the operands is false.
-
nnf.operators.
nor
(a: nnf.NNF, b: nnf.NNF) → nnf.And[nnf.NNF][nnf.NNF][source]¶ Both of the operands are false.
-
nnf.operators.
implies
(a: nnf.NNF, b: nnf.NNF) → nnf.Or[nnf.NNF][nnf.NNF][source]¶ b
is true whenevera
is true.
-
nnf.operators.
implied_by
(a: nnf.NNF, b: nnf.NNF) → nnf.Or[nnf.NNF][nnf.NNF][source]¶ a
is true wheneverb
is true.
-
nnf.operators.
iff
(a: nnf.NNF, b: nnf.NNF) → nnf.Or[nnf.And[nnf.NNF]][nnf.And[nnf.NNF][nnf.NNF]][source]¶ a
is true if and only ifb
is true.
nnf.dimacs module¶
A parser and serializer for the DIMACS CNF and SAT formats.
-
nnf.dimacs.
dump
(obj: nnf.NNF, fp: TextIO, *, num_variables: Optional[int] = None, var_labels: Optional[Dict[Hashable, int]] = None, comment_header: Optional[str] = None, mode: str = 'sat') → None[source]¶ Dump a sentence into an open file in a DIMACS format.
Variable names have to be integers. If the variables in the sentence you want to dump are not integers, you can pass a
var_labels
dictionary to map names to integers.Parameters: - obj – The sentence to dump.
- fp – The open file.
- num_variables – Override the number of variables, in case there are variables that don’t appear in the sentence.
- var_labels – A dictionary mapping variable names to integers, to rename non-integer variables.
- comment_header – A comment to include at the top of the file. May include newlines.
- mode – Either
'sat'
to dump in the general SAT format, or'cnf'
to dump in the specialized CNF format.
-
nnf.dimacs.
load
(fp: TextIO) → Union[nnf.NNF, nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]]][source]¶ Load a sentence from an open file.
The format is automatically detected.
-
nnf.dimacs.
dumps
(obj: nnf.NNF, *, num_variables: Optional[int] = None, var_labels: Optional[Dict[Hashable, int]] = None, comment_header: Optional[str] = None, mode: str = 'sat') → str[source]¶ Like
dump()
, but to a string instead of to a file.
-
nnf.dimacs.
loads
(s: str) → Union[nnf.NNF, nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]]][source]¶ Like
load()
, but from a string instead of from a file.
-
exception
nnf.dimacs.
EncodeError
[source]¶ Bases:
nnf.dimacs.DimacsError
-
exception
nnf.dimacs.
DecodeError
[source]¶ Bases:
nnf.dimacs.DimacsError
nnf.dsharp module¶
Interoperability with DSHARP.
load
and loads
can be used to parse files created by DSHARP’s
-Fnnf
option.
compile
invokes DSHARP directly to compile a sentence. This requires
having DSHARP installed.
The parser was derived by studying DSHARP’s output and source code. This format might be some sort of established standard, in which case this parser might reject or misinterpret some valid files in the format.
DSHARP may not work properly for some (usually trivially) unsatisfiable sentences, incorrectly reporting there’s a solution. This bug dates back to sharpSAT, on which DSHARP was based:
https://github.com/marcthurley/sharpSAT/issues/5
It was independently discovered by hypothesis during testing of this module.
-
nnf.dsharp.
load
(fp: TextIO, var_labels: Optional[Dict[int, Hashable]] = None) → nnf.NNF[source]¶ Load a sentence from an open file.
An optional
var_labels
dictionary can map integers to other names.
-
nnf.dsharp.
loads
(s: str, var_labels: Optional[Dict[int, Hashable]] = None) → nnf.NNF[source]¶ Load a sentence from a string.
-
nnf.dsharp.
compile
(sentence: nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]], executable: str = 'dsharp', smooth: bool = False, timeout: Optional[int] = None, extra_args: Sequence[str] = ()) → nnf.NNF[source]¶ Run DSHARP to compile a CNF sentence to (s)d-DNNF.
This requires having DSHARP installed.
The returned sentence will be marked as deterministic.
Parameters: - sentence – The CNF sentence to compile.
- executable – The path of the
dsharp
executable. If the executable is in your PATH there’s no need to set this. - smooth – Whether to produce a smooth sentence.
- timeout – Tell DSHARP to give up after a number of seconds.
- extra_args – Extra arguments to pass to DSHARP.
nnf.amc module¶
An implementation of algebraic model counting.
-
nnf.amc.
eval
(node: nnf.NNF, add: Callable[[T, T], T], mul: Callable[[T, T], T], add_neut: T, mul_neut: T, labeling: Callable[[nnf.Var], T]) → T[source]¶ Execute an AMC technique, given a semiring and a labeling function.
Parameters: - node – The sentence to calculate the value of.
- add – The ⊕ operator, to combine
nnf.Or
nodes. - mul – The ⊗ operator, to combine
nnf.And
nodes. - add_neut – e^⊕, the neutral element of the ⊕ operator.
- mul_neut – e^⊗, the neutral element of the ⊗ operator.
- labeling – The labeling function, to assign a value to each variable node.
-
nnf.amc.
reduce
(node: nnf.NNF, add_key: Optional[Callable[[T], Any]], mul: Callable[[T, T], T], add_neut: T, mul_neut: T, labeling: Callable[[nnf.Var], T]) → nnf.NNF[source]¶ Execute AMC reduction on a sentence.
In AMC reduction, the ⊕ operator must be
max
on some total order, and the branches of the sentence that don’t contribute to the maximum value are removed. This leaves a simpler sentence with only the models with a maximum value.Parameters: Returns: The transformed sentence.
-
nnf.amc.
NUM_SAT
(node: nnf.NNF) → int[source]¶ Determine the number of models that satisfy a sd-DNNF sentence.
-
nnf.amc.
WMC
(node: nnf.NNF, weights: Callable[[nnf.Var], float]) → float[source]¶ Model counting of sd-DNNF sentences, weighted by variables.
Parameters: - node – The sentence to measure.
- weights – A dictionary mapping variable nodes to weights.
-
nnf.amc.
PROB
(node: nnf.NNF, probs: Dict[Hashable, float]) → float[source]¶ Model counting of d-DNNF sentences, weighted by probabilities.
Parameters: - node – The sentence to measure.
- probs – A dictionary mapping variable names to probabilities.
-
nnf.amc.
GRAD
(node: nnf.NNF, probs: Dict[Hashable, float], k: Optional[Hashable] = None) → Tuple[float, float][source]¶ Calculate a gradient of a d-DNNF sentence being true depending on the value of a variable, given probabilities for all variables.
Parameters: - node – The sentence.
- probs – A dictionary mapping variable names to probabilities.
- k – The name of the variable to check relative to.
Returns: A tuple of two floats (probability, gradient).
nnf.tseitin module¶
Transformations using the well-known Tseitin encoding.
The Tseitin transformation converts any arbitrary circuit to one in CNF in polynomial time/space. It does so at the cost of introducing new variables (one for each logical connective in the formula).
nnf.kissat module¶
Interoperability with kissat.
solve
invokes the SAT solver directly on the given theory.
nnf.pysat module¶
-
nnf.pysat.
satisfiable
(sentence: nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]]) → bool[source]¶ Return whether a CNF sentence is satisfiable.
-
nnf.pysat.
solve
(sentence: nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]]) → Optional[Dict[Hashable, bool]][source]¶ Return a model of a CNF sentence, or
None
if unsatisfiable.
-
nnf.pysat.
models
(sentence: nnf.And[nnf.Or[nnf.Var]][nnf.Or[nnf.Var][nnf.Var]]) → Iterator[Dict[Hashable, bool]][source]¶ Yield all models of a CNF sentence.
-
nnf.pysat.
available
= False¶ Indicates whether the PySAT library is installed and available for use.