Quantified Boolean formula manipulation (pyqbf.formula)

List of classes

PCNF	Class for manipulating PCNF formulas.
QCIRGateType	Possible types for gates of quantified circuits (QCIR)
QCIRGate	Represents a gate in a quantified circuit (QCIR)
QCIR	Class for manipulating quantified Circuit (QCIR) formulas.

List of methods

split_atoms_and_auxvars	Computes the atoms (literals) and auxvars (tseitin-variables) from the given pysat.formula.Formula using the internal pysat.formula.IDPool.
to_pcnf	Safely transforms the input to a PCNF class.

List of constants

QUANTIFIER_FORALL	Indicator for an universial quantifier
QUANTIFIER_EXISTS	Indicator for an existential quantifier
QUANTIFIER_NONE	Indicator for a free variable
OUTERMOST_BLOCK	Indicator for the outermost quantifier block
INNERMOST_BLOCK	Indicator for the innermost quantifier block

Module description

This module provides classes and methods for simple manipulation of quantified boolean formulas in prenex normal form, where the propositional part of the formula is in conjunctive normal form (CNF), i.e. PCNF.

We can see PCNF as an extension of CNF with the addition of a quantifier-prefix. Therefore, the PCNF-class inherits all the properties provided by pysat.formula.CNF with the additional prefix-attribute. The prefix can be set using the forall() and exists() functions

The propositional part can be seen as a set of clauses, where each clause is a set of literals. Literals are represented using the int type, where a negative value indicates the negation of the variable referenced.

The prefix can be seen as an ordered tuple of quantifiers. The order-relation applied to the quantifier is expressed by the order of where the variable occur in the prefix. A negative value indicates forall-quantification whereas a postive value indicates exists.

>>> from pyqbf.formula import PCNF
>>> pcnf = PCNF()
>>> pcnf.append([-1, 2])
>>> pcnf.append([-2, 3])
>>> pcnf.forall(1).exists(2, 3)
>>> print(pcnf.clauses)
[[-1, 2], [-2, 3]]
>>> print(pcnf.prefix)
[-1, 2, 3]
>>> print(pcnf.nv)
3

The default input-format is QDIMACS. Very similar to DIMACS for PySAT, reading and writing can be done the following way:

>>> from pyqbf.formula import PCNF
>>> f1 = PCNF(from_file="some-file-name.qdimacs") 
>>> f1.to_file("another-file-name.qdimacs")
>>>
>>> with open('some-file-name.qdimacs', 'r+') as fp:
...     f2 = PCNF(from_fp=fp)
...
...     fp.seek(0)
...     f2.to_fp(fp)
>>>
>>> f3 = PCNF(from_string="p cnf 3 3\na 1 0\ne 2 3 0\n-1 2 0\n-2 3 0\n-3 0\n")
>>> print(f3.clauses)
[[-1, 2], [-2, 3], [-3]]
>>> print(f3.prefix)
[-1, 2, 3]
>>> print(f3.nv)
3

PyQBF furthermore allows easy extensions from the domain of Propositional Logic into QBF. In the following are a few examples.

>>> from pyqbf.formula import PCNF, to_pcnf
>>> f1 = PCNF(from_file="cnf.dimacs")   #DIMACS is compatible with QDIMACS
>>> print(f1.prefix)                    #but the prefix is empty
[]
>>> f1.forall(1).exists(2,3,4).forall(5,6)
>>> print(f1.prefix)
[-1, 2, 3, 4, -5, -6]
>>>
>>> f2 = PCNF(from_file="cnf.dimacs", auto_generate_prefix=True)
>>> print(f2.prefix)                    #now everything is automatically existentially quantified
[1, 2, 3, 4, 5, 6]
>>> f2.set_quantifier(1, QUANTIFIER_FORALL)
>>> print(f2.prefix)
[-1, 2, 3, 4, 5, 6]

Note

Currently only the pysat.formula.CNF class is supported. More complex structures like pysat.formula.WCNF or pysat.formula.CNFPlus can not be expressed using quantification at the moment.

Module details

pyqbf.formula.INNERMOST_BLOCK = None

Indicator for the innermost quantifier block

pyqbf.formula.OUTERMOST_BLOCK = 0

Indicator for the outermost quantifier block

class pyqbf.formula.PCNF(*args, **kwargs)

Bases: CNF

Class for manipulating PCNF formulas. It can be used for creating formulas, reading them from a file, or writing them to a file.

Parameters:

• from_file (str) – a QDIMACS filename to read from

• from_fp (SupportsRead[str]) – a file pointer to read from

• from_string (str) – a string storing a PCNF formula in QDIMACS format

• from_clauses (list[list[int]]) – a list of clauses to bootstrap the formula with. Variables are free by default

• from_aiger (aiger.AIG (see py-aiger package)) – an AIGER circuit to bootstrap the formula with. Variables are free by default

• from_cnf (pysat.formula.CNF) – a CNF-formula. Variables are free by default

• auto_generate_prefix (bool) – if true, a prefix is automatically generated from the propositional part.

Variables:

• prefix (list[int]) – Prefix of the formula containing the quantifications

• clauses (list[list[int]]) – Propositional part of the formula containing the clauses

• comments (list[str]) – Comments encountered during parsing

• nv (int) – Total count of variables

append(clause, update_vpool=False)

Add one more clauses to the PCNF formula. This method additionally updates the number of variables, i.e. variable self.nv, used in the formula.

The additional keyword argument update_vpool can be set to True if the user wants to update for default static pool of variable identifiers stored in class Formula. In light of the fact that a user may encode their problem manually and add thousands to millions of clauses using this method, the value of update_vpool is set to False by default.

Note

Setting update_vpool=True is required if a user wants to combine this PCNF formula with other (clausal or non-clausal) formulas followed by the clausification of the result combination. Alternatively, a user may resort to using the method extend() instead.

Parameters:

• clause (list[int]) – a new clause to add

• update_vpool (bool) – update or not the static vpool

>>> from pyqbf.formula import PCNF
>>> pcnf = PCNF(from_clauses=[[-1, 2], [3]])
>>> pcnf.append([-3, 4])
>>> print(pcnf.clauses)
[[-1, 2], [3], [-3, 4]]

block_of(var)

Computes the block the specified variable is in. If the variable is free or does not occur in the formula, OUTERMOST_BLOCK is returned.

Parameters:

var (int) – The variable the block is to be computed of

Returns:

the index of the block the variable occurs in

Return type:

int

copy()

This method can be used for creating a copy of a PCNF object. It creates another object of the PCNF class and makes use of the deepcopy() functionality to copy the prefix and clauses.

Returns:

A copy of the current instance.

Return type:

PCNF

Usage example:

>>> pcnf1 = PCNF(from_clauses=[[-1, 2], [1]])
>>> pcnf1.forall(1).exists(2)
>>> pcnf2 = pcnf1.copy()
>>> print(pcnf2.prefix)
[-1, 2]
>>> print(pcnf2.clauses)
[[-1, 2], [1]]
>>> print(pcnf2.nv)
2

count_quantifier_alternations()

Computes the amount of quantifier alternations of the current prefix

Returns:

the number of quantifier alternations

Return type:

int

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> p.count_quantifier_alternations()
1
>>> p.exists(4).forall(5,6)
>>> p.count_quantifier_alternations()
2

exists(*vars, block=None)

Adds variables bound by an existential quantifier to the formula’s prefix. Optionally, specify the block-parameter to add it to the front of the block at the specified index. You can also use the special indicess :class:OUTERMOST_BLOCK and :class:INNERMOST_BLOCK If the variable already exists in the prefix, it is removed at the old position

Parameters:

vars (int) – identifiers of the variables

Returns:

The current PCNF for chaining

Return type:

PCNF

Usage example:

>>> pcnf = PCNF()
>>> pcnf.exists(1, 2, "3", 4.0).exists(5)
>>> qlist = [6, 7, 8, 9]
>>> pcnf.exists(*qlist)
>>> print(pcnf.prefix)
[1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> pcnf.exists(10, block=OUTERMOST_BLOCK)
>>> print(pcnf.prefix)
[10, 1, 2, 3, 4, 5, 6, 7, 8, 9]
>>> pcnf.exists(11, block=1)
[10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11]

extend(clauses)

Add several clauses to PCNF formula. The clauses should be given in the form of list. For every clause in the list, method append() is invoked.

Parameters:

clauses (:class`list[list[int]]`) – a list of new clauses to add

Usage example:

>>> from pyqbf.formula import PCNF
>>> pcnf = PCNF(from_clauses=[[-1, 2], [3]])
>>> pcnf.extend([[-3, 4], [5, 6]])
>>> print(pcnf.clauses)
[[-1, 2], [3], [-3, 4], [5, 6]]

flip_quantifier(*vars)

Flips the quantifier of the specified variables (\(\exists \Rightarrow \forall\), \(\forall \Rightarrow \exists\)). If a variable is free, nothing changes.

Parameters:

vars – identifiers of the variable

Usage example:

>>> pcnf = PCNF(...)
>>> print(pcnf.prefix)
[1, -2, 3, ...]
>>> pcnf.fip_quantifier(1)
>>> print(pcnf.prefix)
[-1, -2, 3, ...]
>>> pcnf.fip_quantifier(1, 2, 3)
>>> print(pcnf.prefix)
[1, 2, -3, ...]        

forall(*vars, block=None)

Adds variables bound by an universial quantifier to the formula’s prefix. Optionally, specify the block-parameter to add it to the front of the block at the specified index. You can also use the special indicess :class:OUTERMOST_BLOCK and :class:INNERMOST_BLOCK If the variable already exists in the prefix, it is removed at the old position

Parameters:

• vars (int) – identifiers of the variables

• block – index of the block to be added to.

Returns:

The current PCNF for chaining

Return type:

PCNF

Usage example:

>>> pcnf = PCNF()
>>> pcnf.forall(1, 2, "3", 4.0).forall(5)
>>> qlist = [6, 7, 8, 9]
>>> pcnf.forall(*qlist)
>>> print(pcnf.prefix)
[-1, -2, -3, -4, -5, -6, -7, -8, -9]
>>> pcnf.forall(10, block=OUTERMOST_BLOCK)
>>> print(pcnf.prefix)
[-10, -1, -2, -3, -4, -5, -6, -7, -8, -9]
>>> pcnf.forall(11, block=1)
[-10, -1, -2, -3, -4, -5, -6, -7, -8, -9, -11]

from_aiger(aig, vpool=False)

Create a PCNF formula by Tseitin-encoding an input AIGER circuit.

The input circuit is expected to be an object of class aiger.AIG. Alternatively, it can be specified as an aiger.BoolExpr, an *.aag filename or an AIGER string to parse. (Classes aiger.AIG and aiger.BoolExpr are defined in the py-aiger package.)

Parameters:

• aig (aiger.AIG (see py-aiger package)) – an input AIGER circuit

• vpool (IDPool) – pool of variable identifiers (optional)

Usage example:

>>> import aiger
>>> x, y, z = aiger.atom('x'), aiger.atom('y'), aiger.atom('z')
>>> expr = ~(x | y) & z
>>> print(expr.aig)
aag 5 3 0 1 2
2
4
8
10
6 3 5
10 6 8
i0 y
i1 x
i2 z
o0 6c454aea-c9e1-11e9-bbe3-3af9d34370a9
>>>
>>> from pyqbf.formula import PCNF
>>> pcnf = PCNF(from_aiger=expr.aig)
>>> print(pcnf.nv)
5
>>> print(pcnf.clauses)
[[3, 2, 4], [-3, -4], [-2, -4], [-4, -1, 5], [4, -5], [1, -5]]
>>> print(['{0} <-> {1}'.format(v, pcnf.vpool.obj(v)) for v in pcnf.inps])
['3 <-> y', '2 <-> x', '1 <-> z']
>>> print(['{0} <-> {1}'.format(v, pcnf.vpool.obj(v)) for v in pcnf.outs])
['5 <-> 6c454aea-c9e1-11e9-bbe3-3af9d34370a9']

from_clauses(clauses, by_ref=False)

This methods copies a list of clauses into a PCNF object. The optional keyword argument by_ref (False by default) indicates whether the clauses should be deep-copied or copied by reference.

Parameters:

• clauses (list(list(int))) – a list of clauses

• by_ref (bool) – a flag to indicate whether to deep-copy the clauses or copy them by reference

Usage example:

>>> from pyqbf.formula import PCNF
>>> pcnf = PCNF(from_clauses=[[-1, 2], [1, -2], [5]])
>>> print(pcnf.clauses)
[[-1, 2], [1, -2], [5]]
>>> print(pcnf.nv)
5

from_file(fname, comment_lead=['c'], compressed_with='use_ext')

Read a PCNF formula from a file in the QDIMACS format. A file name is expected as an argument. A given file can be compressed by either gzip, bzip2, or lzma.

Note

The parameter comment_lead exists due to compatibility with pysat.formula.CNF.from_file() but does not serve a purpose here

Parameters:

• fname (str) – name of a file to parse.

• comment_lead (list(str)) – a list of characters leading comment lines

• compressed_with (str) – file compression algorithm

Note that the compressed_with parameter can be None (i.e. the file is uncompressed), 'gzip', 'bzip2', 'lzma', or 'use_ext'. The latter value indicates that compression type should be automatically determined based on the file extension. Using 'lzma' in Python 2 requires the backports.lzma package to be additionally installed.

Usage example:

>>> from pyqbf.formula import PCNF
>>> pcnf1 = PCNF()
>>> pcnf1.from_file('some-file.qcnf.gz', compressed_with='gzip')
>>>
>>> cnf2 = CNF(from_file='another-file.qcnf')

from_fp(file_pointer, comment_lead=[])

Read a PCNF formula in QDIMACS format from a file pointer.

Note

The parameter comment_lead exists due to compatibility with pysat.formula.CNF.from_fp() but does not serve a purpose here

Parameters:

• file_pointer (SupportsRead[str]) – a file pointer to read the formula from.

• comment_lead (list[str]) – a list of characters leading comment lines (for compatibility reason)

Usage example:

>>> with open('some-file.qdimacs', 'r') as fp:
...     pcnf1 = PCNF()
...     pcnf1.from_fp(fp)
>>>
>>> with open('another-file.qdimacs', 'r') as fp:
...     pcnf2 = PCNF(from_fp=fp)

from_string(string, comment_lead=['c'])

Read a PCNF formula from a string. The string should be specified as an argument and should be in the QDIMACS PCNF format. The only default argument is comment_lead, which can be used for parsing specific comment lines.

Parameters:

• string (str) – a string containing the formula in QDIMACS.

• comment_lead (list(str)) – a list of characters leading comment lines

Usage example:

>>> from pyqbf.formula import PCNF
>>> pcnf1 = PCNF()
>>> pcnf1.from_string('p cnf 2 2\na 1 0\ne 2 0\n-1 2 0\n1 -2 0')
>>> print(pcnf1.clauses)
[[-1, 2], [1, -2]]
>>>
>>> print(pcnf1.prefix)
[-1, 2]
>>> pcnf2 = PCNF(from_string='p cnf 3 3\n-1 2 0\n-2 3 0\n-3 0\n')
>>> print(pcnf2.clauses)
[[-1, 2], [-2, 3], [-3]]
>>> print(pcnf2.nv)
3)
>>> print(pcnf2.prefix)
[]

generate_blocks()

Computes a representation of the quantifier blocks as generator

Returns:

a generator for a list of lists representing the quantifier blocks

Return type:

list[list[int]]

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> print(list(p.generate_blocks()))
[[-1], [2, 3]]

get_block(b)

Returns the quantifier block in index b. If there is no block on this index, an empty list is returned You can also use the special indicess :class:OUTERMOST_BLOCK and :class:INNERMOST_BLOCK

Parameters:

b (int) – index of the block to be computed

Returns:

a list representing the block at index b

Return type:

list[int]

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> p.get_block(1)
[2,3]
>>> p.exists(4).forall(5,6)
>>> p.get_block(2)
[-5,-6]
>>> p.get_block(3)
[]

get_block_type(b)

Returns the type of the quantifier block on index b. If there is no block on this index or the block is empty, QUANTIFIER_NONE is returned You can also use the special indicess :class:OUTERMOST_BLOCK and :class:INNERMOST_BLOCK

Parameters:

b (int) – index of the block to be computed

Returns:

returns:

QUANTIFIER_EXISTS, QUANTIFIER_FORALL or QUANTIFIER_NONE

Return type:

int

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> print(pcnf.get_block_type(0) == QUANTIFIER_FORALL)
True
>>> print(pcnf.get_block_type(1) == QUANTIFIER_EXISTS)
True
>>> print(pcnf.get_block_type(2) == QUANTIFIER_NONE)
True

innermost_block(qtype=0)

Returns the innermost quantifier block of the specified type. If QUANTIFIER_NONE is specified as a type, the last block regardless of quantifier will be returned.

Parameters:

qtype (int) – QUANTIFIER_EXISTS, QUANTIFIER_FORALL or QUANTIFIER_NONE

Returns:

a list representing the innermost block

Return type:

list[int]

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> p.innermost_block()
[2,3]
>>> p.innermost_block(QUANTIFIER_EXISTS)
[2,3]
>>> p.innermost_block(QUANTIFIER_FORALL)
[-1]
>>> p.exists(4).forall(5,6)
>>> p.innermost_block()
[-5,-6]
>>> p.innermost_block(QUANTIFIER_EXISTS)
[2,3,4]
>>> p.innermost_block(QUANTIFIER_FORALL)
[-5,-6]

introduce_var(quantifier=1, block=None)

Introduces a new variable on a unique id at the specified position

Parameters:

• quantifier (int) – specifies the quantifier type of the variable (optional)

• block (int) – specifies the block, the variable is instantiated into

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]], auto_generate_prefix=True)
>>> print(pcnf.nv)
2
>>> var = pcnf.introduce_var()
>>> print(var)
3
>>> var2 = pcnf.introduce_var(quantifier=QUANTIFIER_FORALL)
>>> print(var2)
4
>>> var3 = pcnf.introduce_var(quantifier=QUANTIFIER_FORALL, block=OUTERMOST_BLOCK)
>>> print(var3)
5
>>> print(pcnf.prefix)
[-5, 1, 2, 3, -4]
>>> print(pcnf.nv)
5

property is_normalized

Indicates whether the formula was normalized. This is needed for certain solvers like pyqbf.solvers.Qute.

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2, 3], [-1, 2, 3], [-1, -2, -3]])
>>> print(pcnf.is_normalized)
False
>>> pcnf.normalize()
>>> print(pcnf.is_normalized)
True

minimize_prefix()

Removes all unnecessary variables from the prefix.

Usage Exaple:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]])
>>> pcnf.forall(1,2,3).exists(4,5,6)
>>> print(pcnf.prefix)
[-1, -2, -3, 4, 5, 6]
>>> pcnf.minimize_prefix()
>>> print(pcnf.prefix)
[-1, -2]

negate()

Given a PCNF formula \(\mathcal{F}\), this method creates a PCNF formula \(\neg{\mathcal{F}}\).

The negation of the propositional part is encoded using additional Tseitin variables [1]. Furthermore, the technique proposed by Plaisted and Greenbaum [2] is used to reduce the amount of clauses. For the prenex, the quantifiers are inversed, i.e. existential become universial and vice versa. A new PCNF formula is returned keeping all the newly introduced variables that can be accessed through the auxvars variable. All the literals used to encode the negation of the original clauses can be accessed through the enclits variable.

If this function is called twice and the encoding can still be re-constructed, instead of re-encoding with another set of tseitin variables it will reverse the encoding and restore the original formula.

Returns:

a formula describing the negated version of the input

Return type:

PCNF

[1]

G. S. Tseitin. On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic, Part II. pp. 115–125, 1968

[2]

Plaisted, D.A., Greenbaum, S. A structure-preserving clause form translation. Journal of Symbolic Computation 2(3), 293–304 (1986)

>>> pos = PCNF(from_clauses=[[-1, 2], [3]])
>>> pos.forall(1).exists(2,3)
>>> neg = pos.negate()
>>> print(neg.prefix)
[1, -2, -3, 4]
>>> print(neg.clauses)
[[1, -4], [-2, -4], [4, -3]]
>>> print(neg.auxvars)
[4]
>>> print(neg.enclits)
[4, -3]
>>> pos2 = neg.negate()
>>> print(pos2.prefix)
[-1, 2, 3]
>>> print(pos2.clauses)
[[-1, 2], [3]]

normalize()

Normalizes the current formula. Free variables are eliminated by adding them to the prefix. Variable-ids are assigned by the order they are defined such that there are no gaps.

Usage example:

>>> pcnf = PCNF(from_clauses=[[-2, 4], [-4, 6], [-6, 2]])
>>> pcnf.forall(6)
>>> print(pcnf.nv)
6
>>> pcnf.normalize()   # eliminate free variables and re-map ids
>>> print(pcnf.prefix) # 2 => 1, 4 => 2, 6 => 3
[1, 2, -3]
>>> print(pcnf.clauses)
[[-1, 2], [-2, 3], [-3, 1]]
>>> print(pcnf.nv)
3

outermost_block(qtype=0)

Returns the outermost quantifier block of the specified type. If QUANTIFIER_NONE is specified as a type, the first block regardless of quantifier will be returned.

Parameters:

qtype (int) – QUANTIFIER_EXISTS, QUANTIFIER_FORALL or QUANTIFIER_NONE

Returns:

a list representing the outermost block

Return type:

list[int]

Usage example:

>>> from pyqbf.formula import PCNF
>>> p = PCNF(from_clauses=[[-1, 2], [3]])
>>> p.forall(1).exists(2,3)
>>> p.outermost_block()
[-1]
>>> p.outermost_block(QUANTIFIER_EXISTS)
[2,3]
>>> p.outermost_block(QUANTIFIER_FORALL)
[-1]
>>> p.exists(4, block=OUTERMOST_BLOCK).forall(5,6, block=OUTERMOST_BLOCK)
>>> p.outermost_block()
[-5,-6]
>>> p.outermost_block(QUANTIFIER_EXISTS)
[4]
>>> p.outermost_block(QUANTIFIER_FORALL)
[-5,-6]

prefix_from_clauses(quantifier=1)

Generates the prefix from the clauses specified. The order is determined by the order they occur in the formula

Parameters:

quantifier (int) – the quantifier type the variables should be quantified with. Default QUANTIFIER_EXISTS

>>> pcnf = PCNF(from_clauses=[[1, 2], [-4, 3]])
>>> print(pcnf.prefix)
[]
>>> pcnf.prefix_from_clauses()
>>> print(pcnf.prefix)
[1, 2, 3, 4]
>>> pcnf.prefix_from_clauses(QUANTIFIER_FORALL)
>>> print(pcnf.prefix)
[-1, -2, -3, -4]
>>> # Setting a flag can do this automatically during initialization
>>> pcnf2 = PCNF(from_clauses=[[1, 2], [-4, 3]], auto_generate_prefix=True) 
>>> print(pcnf2.prefix)  
[1, 2, 3, 4]

quantify_free_variables(quantifier=1)

Quantification of free variables by adding them to the prefix.

Parameters:

quantifier (int) – the quantifier type the variables should be quantified with. Default QUANTIFIER_EXISTS

Usage example:

>>> pcnf = PCNF(from_clauses=[[1, 2, 3], [-1, 2, 3], [-1, -2, -3]])
>>> pcnf.forall(1)
>>> print(pcnf.prefix)
[-1]
>>> print(pcnf.nv)
3
>>> pcnf.quantify_free_variables()
>>> print(pcnf.prefix)
[2, 3, -1] 
>>> # free variables are added at the front
>>> print(pcnf.nv)
3
>>> pcnf = PCNF(from_clauses=[[1, 2, 3], [-1, 2, 3], [-1, -2, -3]])
>>> pcnf.forall(1)
>>> pcnf.quantify_free_variables(QUANTIFIER_FORALL)
>>> print(pcnf.prefix)
[-2, -3, -1] 

set_quantifier(var, quantifier=1)

Changes the quantifier of the specified variable to the value specified. If the target is not in the prefix yet, it is appended.

Parameters:

• var (int) – identifier of the variable

• quantifier (int) – type of the quantifier. QUANTIFIER_NONE is not supported

Usage example:

>>> pcnf = PCNF(...)
>>> pcnf.set_quantifier(1, QUANTIFIER_EXISTS)
>>> pcnf.set_quantifier(2, QUANTIFIER_FORALL)
>>> pcnf.set_quantifier(3)  
>>> print(pcnf.prefix)
[1, -2, 3, ...]
>>> pcnf.set_quantifier(2, QUANTIFIER_EXISTS)
[1, 2, 3, ...]

sort_clauses()

Sorts clauses according to the order relation given by the prefix (var_order_relation()). Literals which are not in the prefix (free variables) are inserted at the beginning

Usage Exaple:

>>> pcnf = PCNF(from_clauses=[[1, 2], [-1, -2]])
>>> pcnf.forall(2).exists(1)
>>> print(pcnf.prefix)
[-2, -1]
>>> pcnf.sort_clauses()
>>> print(pcnf.clauses)
[[2, 1], [-2, -1]]

to_alien(file_pointer, format='opb', comments=None)

Warning

This method is currently not supported for PCNF-formulas

Raises:

NotImplementedError

to_file(fname, comments=None, compress_with='use_ext')

A method for saving a PCNF formula into a file in the QDIMACS format. A file name is expected as an argument. Additionally, supplementary comment lines can be specified in the comments parameter. Also, a file can be compressed using either gzip, bzip2, or lzma (xz).

Parameters:

• fname (str) – a file name where to store the formula.

• comments (list[str]) – additional comments to put in the file.

• compress_with (str) – file compression algorithm

Note that the compress_with parameter can be None (i.e. the file is uncompressed), 'gzip', 'bzip2', 'lzma', or 'use_ext'. The latter value indicates that compression type should be automatically determined based on the file extension. Using 'lzma' in Python 2 requires the backports.lzma package to be additionally installed.

Usage example:

>>> pcnf = PCNF()            ...
>>> # the formula is filled with a bunch of clauses and a prefix
>>> pcnf.to_file('some-file-name.qcnf')  # writing to a file

to_fp(file_pointer, comments=None)

The method can be used to save a PCNF formula into a file pointer using QDIMACS encoding. Additional comment lines can be specified with the comments parameter.

Parameters:

• file_pointer (SupportsWrite[str] (file pointer)) – a file pointer where to store the formula.

• comments (list[str]) – additional comments to put in the file.

Usage example:

>>> pcnf = PCNF()
>>> with open("file.qdimacs", "w") as fp:
...    pcnf.to_fp(fp)

to_qdimacs()

Return the current state of the object in QDIMACS encoding.

Returns:

a QDIMACS representation of the formula

Return type:

str

Usage example:

>>> pcnf = PCNF(from_file="some-file.qdimacs")
>>> print(pcnf.comments)
["c First Comment", "c Another Comment"]
>>> print(pcnf.to_qdimacs())
c First Comment
c Another Comment
p cnf 3 3 
a 1 0
e 2 3 0
-1 2 0
-2 3 0
-3 0

var_order_relation()

Returns an order relation with reference to the prefix, which can be used to order clauses

Returns:

a list containing the order

Return type:

list[int]

Usage Exaple:

>>> pcnf = PCNF(from_file="/path/to/formula.qdimacs")
>>> print(pcnf.prefix)
[2, 3, 1]
>>> order = pcnf.var_order_relation()
>>> print(order)
[None, 3, 1, 2]
>> print(order[1])
3
>> print(order[1] < order[2])
False

var_type(var)

Provides quantifier information for the specified variable.

Parameters:

var (int) – identifier of the variable

Returns:

QUANTIFIER_EXISTS, QUANTIFIER_FORALL or QUANTIFIER_NONE

Return type:

int

Usage example:

>>> pcnf = PCNF()
>>> pcnf.exists(1).forall(2)
>>> print(pcnf.var_type(1))
1
>>> print(pcnf.var_type(1) == QUANTIFIER_EXISTS)
True
>>> print(pcnf.var_type(2))
-1
>>> print(pcnf.var_type(2) == QUANTIFIER_FORALL)
True
>>> print(pcnf.var_type(3))
0
>>> print(pcnf.var_type(3) == QUANTIFIER_NONE)
True

class pyqbf.formula.QCIR(from_fp=None, from_string=None, from_file=None, cleansed=False)

Bases: object

Class for manipulating quantified Circuit (QCIR) formulas. It can be used for creating formulas, reading them from a file, or transforming them to a PCNF.

Parameters:

• from_file (str) – a QCIR filename to read from

• from_fp (SupportsRead[str]) – a file pointer to read from

• from_string (str) – a string storing a QCIR formula in QCIR format

• cleansed (bool) – If True, all variable identifiers are expected to be of integer type

Variables:

• prefix (list[str]) – Prefix of the formula containing the variable names

• output (str) – Output variable of the circuit

• gates (list[QCIRGate]) – List of gates in the circuit

• pcnf (PCNF) – Converted PCNF formula of the circuit (only has a value after calling QCIR.to_pcnf())

append(gate)

Add one more gate to the QCIR.

Parameters:

gate (QCIRGate) – a new gate to add.

>>> qc = QCIR()
>>> qc.append(QCIRGate("g1", QCIRGateType.And, ["v1", "v2"]))
>>> qc.append(QCIRGate("g2", QCIRGateType.And, ["-v1", "-v2"]))
>>> qc.append(QCIRGate("g3", QCIRGateType.Or, ["g1", "g2"]))
>>> len(qc.gates)
3
>>> str(qc.gates[2])
g3 = or(g1,g2)

cleanse()

Cleanses the circuit by replacing str-identifier by int-identifiers. The used mapping can be found in the cleanse_mapping field of the class.

Usage example:

>>> from pyqbf.formula import QCIR
>>> qc = QCIR(from_string='#QCIR-14\nforall(a)\nexists(b)\noutput(out)\nout=and(-a, b)\n')
>>> qc.cleanse()
>>> qc.prefix
[-1, 2]
>>> str(qc.gates[0])
3 = and(-1, 2)
>>> qc.cleanse_mapping
{"a": 1, "b": 2, "out": 3}

extend(gates)

Adds all the given gates to the QCIR.

Parameters:

gates – a list of new gates to add.

>>> qc = QCIR()
>>> qc.extend([QCIRGate("g1", QCIRGateType.And, ["v1", "v2"]),\
...            QCIRGate("g2", QCIRGateType.And, ["-v1", "-v2"]),\
...            QCIRGate("g3", QCIRGateType.Or, ["g1", "g2"])])
>>> len(qc.gates)
3
>>> str(qc.gates[2])
g3 = or(g1,g2)

from_file(fname, cleansed=False)

Read a QCIR formula from a file in the QCIR format. A file name is expected as an argument.

Parameters:

• fname (str) – name of a file to parse.

• cleansed (bool) – if true, assume the contained formula is cleansed

Usage example:

>>> from pyqbf.formula import QCIR
>>> qc1 = QCIR()
>>> qc1.from_file('some-file.qcir')
>>>
>>> qc2 = QCIR(from_file='another-file.cleansed.qcir', cleansed=True)

from_fp(fp, cleansed=False)

Read a QCIR formula from a file pointer. A file pointer should be specified as an argument.

Parameters:

• file_pointer (file pointer) – a file pointer to read the formula from.

• cleansed (bool) – if true, assume the contained formula is cleansed

Usage example:

>>> with open('some-file.qcir', 'r') as fp:
...     qc1 = QCIR()
...     qc1.from_fp(fp)
>>>
>>> with open('another-file.cleansed.qcir', 'r') as fp:
...     qc2 = QCIR(from_fp=fp, cleansed=True)

from_string(string, cleansed=False)

Read a QCIR formula from a string. The string should be specified as an argument and should be in the QCIR format.

Parameters:

• string (str) – a string containing the formula in QCIR.

• cleansed (bool) – if true, assume the contained formula is cleansed

Usage example:

>>> from pyqbf.formula import QCIR
>>> qc1 = QCIR()
>>> qc1.from_string('#QCIR-14\nforall(1)\nexists(2)\noutput(5)\n3=and(-1, 2)\n4=and(1, -2)\n5=or(3,4)\n')
>>> print(qc1.prefix)
['-1', '2']
>>> print(qc1.output)
'5'
>>> qc2.from_string('#QCIR-14\nforall(1)\nexists(2)\noutput(5)\n3=and(-1, 2)\n4=and(1, -2)\n5=or(3,4)\n', cleansed=True)
>>> print(qc1.prefix)
[-1, 2]
>>> print(qc1.output)
5            
>>> qc3 = QCIR(from_string='#QCIR-14\nforall(a)\nexists(b)\noutput(out)\nout=and(-a, b)\n')
>>> print(qc3.prefix)
['-a', 'b']
>>> print(qc3.output)
'out'
>>> print(qc3.gates)
['out = and(-a, b)']

to_file(file, g14_format=False)

Writes the current state of the object in QCIR encoding into the specified file.

Parameters:

• file (str) – a file name where to store the formula.

• g14_format (bool) – if true, the QCIR-G14 format will be used

Usage example:

>>> qc = QCIR(from_file="some-file.qcir")                
>>> qc.to_file('some-other-file.qcir', g14_format=True)

to_fp(fp, g14_format=False)

Writes the current state of the object in QCIR encoding into a file pointer.

Parameters:

• fp (file pointer) – a file pointer where to store the formula.

• g14_format (bool) – if true, the QCIR-G14 format will be used

Usage example:

>>> qc = QCIR(from_file="some-file.qcir")
>>> with open('some-other-file.qcir', 'w') as fp:
...     qc.to_fp(fp) 

to_pcnf() → PCNF

Safely transforms the QCIR to a PCNF. If the QCIR is not cleansed so far, it will be in the process of transforming. The result can also be found in the pcnf-field of the class

Returns:

A formula in PCNF representing the circuit

Return type:

PCNF

Usage example:

>>> qc = QCIR(from_string='#QCIR-14\nforall(a)\nexists(b)\noutput(out)\nout=and(-a, b)\n')
>>> pcnf = qc.to_pcnf()             
>>> qc.cleanse_mapping
{"a": 1, "b": 2, "out": 3}   
>>> print(pcnf.prefix)
[-1, 2]
>>> print(pcnf.clauses)
[[-3, -1], [-3, 2], [3, 1, -2], [3]]                

to_string(g14_format=False)

Return the current state of the object in QCIR encoding.

Parameters:

g14_format (bool) – if true, the QCIR-G14 format will be used

Returns:

a QCIR representation of the formula

Return type:

str

Usage example:

>>> qc = QCIR(from_file="some-file.qcir")
>>> print(qc.to_string())
#QCIR-14
forall(a)
exists(b)
output(o)
o = and(a,b)
>>> print(qc.to_string(g14_format=True))
#QCIR-G14 1
forall(a)
exists(b)
output(o)
o = and(a,b)

class pyqbf.formula.QCIRGate(vid, gtype, children=[], cleansed=False)

Bases: object

Represents a gate in a quantified circuit (QCIR)

Parameters:

• vid (str | int) – The non-negative variable identifier for this gate. Can be a str or, if cleansed, an int

• gtype (QCIRGateType) – The type of the gate

• children (list[str] | list[int]) – A list containing variable identifiers describing the members of the gate. Can be a list[str] or, if cleansed, an list[int]

• cleansed (bool) – Indicates whether this gate was cleansed (i.e. only contains integer ids)

Usage example:

>>> g = QCIRGate("g1", QCIRGateType.And, ["v1", "v2"])
>>> g.vid 
"g1"
>>> g.type
QCIRGateType.And
>>> g.children
["v1", "v2"]
>>> mapping = {"g1": 3, "v1": 1, "v2": 2}
>>> g.cleanse(mapping)
>>> print(str(g))
"3 = and(1,2)"
>>> pcnf = PCNF()
>>> g.to_pcnf(pcnf)
>>> print(pcnf.clauses)
[[-3, 1], [-3, 2], [3, -1, -2]]

cleanse(mapping)

Cleanses the gate according to the provided mapping. Note that all occurring identifier have to be available in the mapping

Parameters:

mapping (dict[str,int]) – Mapping from str identifier to int

Usage example:

>>> g = QCIRGate("g1", QCIRGateType.And, ["v1", "-v2"])
>>> cleanse_mapping = {"v1": 1, "v2": 2, "g1": 3}
>>> g.cleanse(cleanse_mapping)
>>> g.vid
3
>>> g.children
[1, -2]               

negate()

Negates the current logic of the gate. This is not supported for ITE, as this can not be modelled with only one gate

Returns:

A gate containing the negation of this gate

Return type:

QCIRGate

Usage example:

>>> g = QCIRGate(3, QCIRGateType.And, [1, -2], cleansed=True)
>>> ng = g.negate()
>>> ng
3 = or(-1, 2)
>>> print(-g)
3 = or(-1, 2)

to_pcnf(pcnf)

Converts the gate to clauses and adds it to the specified PCNF

Parameters:

pcnf (PCNF) – The formula, the gate should be added to

Usage example:

>>> g = QCIRGate(3, QCIRGateType.And, [1, -2], cleansed=True)
>>> pcnf = PCNF()
>>> g.to_pcnf(pcnf)
>>> pcnf.clauses
[[-3, 1], [-3, -2], [3, -1, 2]]

class pyqbf.formula.QCIRGateType(value, names=None, *, module=None, qualname=None, type=None, start=1, boundary=None)

Bases: Enum

Possible types for gates of quantified circuits (QCIR)

pyqbf.formula.QUANTIFIER_EXISTS = 1

Indicator for an existential quantifier

pyqbf.formula.QUANTIFIER_FORALL = -1

Indicator for an universial quantifier

pyqbf.formula.QUANTIFIER_NONE = 0

Indicator for a free variable

pyqbf.formula.split_atoms_and_auxvars(f)

Computes the atoms (literals) and auxvars (tseitin-variables) from the given pysat.formula.Formula using the internal pysat.formula.IDPool.

Parameters:

formula (pysat.formula.Formula) – an abstract formula representation

Returns:

a list of atoms and auxvars read from the vpool of the formula

Return type:

tuple[list[int], list[int]]

Usage example:

>>> from pysat.formula import Atom
>>> formula = (Atom('x') & Atom('y')) | Atom('z')
>>> clauses = [c for c in formula]
>>> print(clauses)
[[1, -3], [2, -3], [3, -1, -2], [3, 4]]
>>> atoms, auxvars = split_atoms_and_auxvars(formula)
>>> print(atoms)
[1, 2, 4]
>>> print(auxvars)
[3]

pyqbf.formula.to_pcnf(cnf)

Safely transforms the input to a PCNF class. The following inputs are currently supported for conversion:

• PCNF: (no copy is made)

• pysat.formula.CNF: (variables are existentially quantified)

• list[list[int]]: (variables are existentially quantified)

• pysat.formula.Formula: (variables are existentially quantified, tseitin variables occur at the end of the prefix)

Parameters:

cnf (e.g. pysat.formula.CNF) – target of the domain expansion

Usage example:

>>> cnf = pysat.formula.CNF(from_clauses = [[-1, 2], [-2, 3], [-3, 1]])
>>> pcnf = to_pcnf(cnf)
>>> print(pcnf.prefix)
[1, 2, 3]
>>> print(pcnf.clauses)
[[-1, 2], [-2, 3], [-3, 1]]
>>> clauses = [[-1, 2], [-2, 3], [-3, 1]]
>>> pcnf2 = to_pcnf(clauses)
>>> print(pcnf2.prefix)
[1, 2, 3]
>>> print(pcnf2.clauses)
[[-1, 2], [-2, 3], [-3, 1]]
>>> f = (Atom('x') & Atom('y')) | Atom('z')
>>> pcnf3 = to_pcnf(f)
>>> print(pcnf3.prefix)
[1, 2, 4, 3]
>>> print("Clauses: ", pcnf3.clauses)
[[1, -3], [2, -3], [3, -1, -2], [3, 4]]
>>> print("Atoms:", pcnf3.atoms)
[1, 2, 4]
>>> print("Auxvars:", pcnf3.auxvars)
[3]