Quantified Boolean formula manipulation (pyqbf.formula)

List of classes

PCNF	Class for manipulating PCNF formulas.

List of methods

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

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

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]]

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

exists(*vars)

Adds variables bound by an existential quantifier to the formula’s prefix.

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)

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 (list(list(int))) – a list of new clauses to add

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]]

forall(*vars)

Adds variables bound by an universial quantifier to the formula’s prefix.

Parameters:

vars (int) – identifiers of the variables

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)

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)

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

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

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)
[]

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

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

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, ...]

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.

Example:

>>> from pysat.formula import PCNF
>>> 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_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

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.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)

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]]