Boolean formula manipulation (`pysat.formula`)#

List of classes#

`IDPool`	A simple manager of variable IDs.
`CNF`	Class for manipulating CNF formulas.
`CNFPlus`	CNF formulas augmented with native cardinality constraints.
`WCNF`	Class for manipulating partial (weighted) CNF formulas.
`WCNFPlus`	WCNF formulas augmented with native cardinality constraints.

Module description#

This module is designed to facilitate fast and easy PySAT-development by providing a simple way to manipulate formulas in PySAT. Although only clausal formulas are supported at this point, future releases of PySAT are expected to implement data structures and methods to manipulate arbitrary Boolean formulas. The module implements the CNF class, which represents a formula in conjunctive normal form (CNF).

Recall that a CNF formula is conventionally seen as a set of clauses, each being a set of literals. A literal is a Boolean variable or its negation. In PySAT, a Boolean variable and a literal should be specified as an integer. For instance, a Boolean variable \(x_{25}\) is represented as integer 25. A literal \(\neg{x_{10}}\) should be specified as -10. Moreover, a clause \((\neg{x_2}\vee x_{19}\vee x_{46})\) should be specified as [-2, 19, 46] in PySAT. Unit size clauses are to be specified as unit size lists as well, e.g. a clause \((x_3)\) is a list [3].

CNF formulas can be created as an object of class CNF. For instance, the following piece of code creates a CNF formula \((\neg{x_1}\vee x_2)\wedge(\neg{x_2}\vee x_3)\).

>>> from pysat.formula import CNF
>>> cnf = CNF()
>>> cnf.append([-1, 2])
>>> cnf.append([-2, 3])

The clauses of a formula can be accessed through the clauses variable of class CNF, which is a list of lists of integers:

>>> print(cnf.clauses)
[[-1, 2], [-2 ,3]]

The number of variables in a CNF formula, i.e. the largest variable identifier, can be obtained using the nv variable, e.g.

>>> print(cnf.nv)
3

Class CNF has a few methods to read and write a CNF formula into a file or a string. The formula is read/written in the standard DIMACS CNF format. A clause in the DIMACS format is a string containing space-separated integer literals followed by 0. For instance, a clause \((\neg{x_2}\vee x_{19}\vee x_{46})\) is written as -2 19 46 0 in DIMACS. The clauses in DIMACS should be preceded by a preamble, which is a line p cnf nof_variables nof_clauses, where nof_variables and nof_clauses are integers. A preamble line for formula \((\neg{x_1}\vee x_2)\wedge(\neg{x_2}\vee x_3)\) would be p cnf 3 2. The complete DIMACS file describing the formula looks this:

p cnf 3 2
-1 2 0
-2 3 0

Reading and writing formulas in DIMACS can be done with PySAT in the following way:

>>> from pysat.formula import CNF
>>> f1 = CNF(from_file='some-file-name.cnf')  # reading from file
>>> f1.to_file('another-file-name.cnf')  # writing to a file
>>>
>>> with open('some-file-name.cnf', 'r+') as fp:
...     f2 = CNF(from_fp=fp)  # reading from a file pointer
...
...     fp.seek(0)
...     f2.to_fp(fp)  # writing to a file pointer
>>>
>>> f3 = CNF(from_string='p cnf 3 3\n-1 2 0\n-2 3 0\n-3 0\n')
>>> print(f3.clauses)
[[-1, 2], [-2, 3], [-3]]
>>> print(f3.nv)
3

Besides plain CNF formulas, the pysat.formula module implements an additional class for dealing with partial and weighted partial CNF formulas, i.e. WCNF formulas. A WCNF formula is a conjunction of two sets of clauses: hard clauses and soft clauses, i.e. \(\mathcal{F}=\mathcal{H}\wedge\mathcal{S}\). Soft clauses of a WCNF are labeled with integer weights, i.e. a soft clause of \(\mathcal{S}\) is a pair \((c_i, w_i)\). In partial (unweighted) formulas, all soft clauses have weight 1.

WCNF can be of help when solving optimization problems using the SAT technology. A typical example of where a WCNF formula can be used is maximum satisfiability (MaxSAT), which given a WCNF formula \(\mathcal{F}=\mathcal{H}\wedge\mathcal{S}\) targets satisfying all its hard clauses \(\mathcal{H}\) and maximizing the sum of weights of satisfied soft clauses, i.e. maximizing the value of \(\sum_{c_i\in\mathcal{S}}{w_i\cdot c_i}\).

An object of class WCNF has two variables to access the hard and soft clauses of the corresponding formula: hard and soft. The weights of soft clauses are stored in variable wght.

>>> from pysat.formula import WCNF
>>>
>>> wcnf = WCNF()
>>> wcnf.append([-1, -2])
>>> wcnf.append([1], weight=1)
>>> wcnf.append([2], weight=3)  # the formula becomes unsatisfiable
>>>
>>> print(wcnf.hard)
[[-1, -2]]
>>> print(wcnf.soft)
[[1], [2]]
>>> print(wcnf.wght)
[1, 3]

A properly constructed WCNF formula must have a top weight, which should be equal to \(1+\sum_{c_i\in\mathcal{S}}{w_i}\). Top weight of a formula can be accessed through variable topw.

>>> wcnf.topw = sum(wcnf.wght) + 1  # (1 + 3) + 1
>>> print(wcnf.topw)
5

Note

Although it is not aligned with the WCNF format description, starting with the 0.1.5.dev8 release, PySAT is able to deal with WCNF formulas having not only integer clause weights but also weights represented as floating point numbers. Moreover, negative weights are also supported.

Additionally to classes CNF and WCNF, the module provides the extended classes CNFPlus and WCNFPlus. The only difference between ?CNF and ?CNFPlus is the support for native cardinality constraints provided by the MiniCard solver (see pysat.card for details). The corresponding variable in objects of CNFPlus (WCNFPlus, resp.) responsible for storing the AtMostK constraints is atmosts (atms, resp.). Note that at this point, AtMostK constraints in WCNF can be hard only.

Besides the implementations of CNF and WCNF formulas in PySAT, the pysat.formula module also provides a way to manage variable identifiers. This can be done with the use of the IDPool manager. With the use of the CNF and WCNF classes as well as with the IDPool variable manager, it is pretty easy to develop practical problem encoders into SAT or MaxSAT/MinSAT. As an example, a PHP formula encoder is shown below (the implementation can also be found in examples.genhard.PHP).

from pysat.formula import CNF
cnf = CNF()  # we will store the formula here

# nof_holes is given

# initializing the pool of variable ids
vpool = IDPool(start_from=1)
pigeon = lambda i, j: vpool.id('pigeon{0}@{1}'.format(i, j))

# placing all pigeons into holes
for i in range(1, nof_holes + 2):
    cnf.append([pigeon(i, j) for j in range(1, nof_holes + 1)])

# there cannot be more than 1 pigeon in a hole
pigeons = range(1, nof_holes + 2)
for j in range(1, nof_holes + 1):
    for comb in itertools.combinations(pigeons, 2):
        cnf.append([-pigeon(i, j) for i in comb])

Module details#

class pysat.formula.CNF(from_file=None, from_fp=None, from_string=None, from_clauses=[], from_aiger=None, comment_lead=['c'])#

Class for manipulating CNF formulas. It can be used for creating formulas, reading them from a file, or writing them to a file. The comment_lead parameter can be helpful when one needs to parse specific comment lines starting not with character c but with another character or a string.

Parameters

from_file (str) – a DIMACS CNF filename to read from
from_fp (file_pointer) – a file pointer to read from
from_string (str) – a string storing a CNF formula
from_clauses (list(list(int))) – a list of clauses to bootstrap the formula with
from_aiger (aiger.AIG (see py-aiger package)) – an AIGER circuit to bootstrap the formula with
comment_lead (list(str)) – a list of characters leading comment lines

append(clause)#

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

Parameters: clause (list(int)) – a new clause to add.

>>> from pysat.formula import CNF
>>> cnf = CNF(from_clauses=[[-1, 2], [3]])
>>> cnf.append([-3, 4])
>>> print(cnf.clauses)
[[-1, 2], [3], [-3, 4]]

copy()#

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

Returns: an object of class CNF.

Example:

>>> cnf1 = CNF(from_clauses=[[-1, 2], [1]])
>>> cnf2 = cnf1.copy()
>>> print(cnf2.clauses)
[[-1, 2], [1]]
>>> print(cnf2.nv)
2

extend(clauses)#

Add several clauses to CNF 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 pysat.formula import CNF
>>> cnf = CNF(from_clauses=[[-1, 2], [3]])
>>> cnf.extend([[-3, 4], [5, 6]])
>>> print(cnf.clauses)
[[-1, 2], [3], [-3, 4], [5, 6]]

from_aiger(aig, vpool=None)#

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

Input circuit is expected to be an object of class aiger.AIG. Alternatively, it can be specified as an aiger.BoolExpr, or 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 pysat.formula import CNF
>>> cnf = CNF(from_aiger=expr.aig)
>>> print(cnf.nv)
5
>>> print(cnf.clauses)
[[3, 2, 4], [-3, -4], [-2, -4], [-4, -1, 5], [4, -5], [1, -5]]
>>> print(['{0} <-> {1}'.format(v, cnf.vpool.obj(v)) for v in cnf.inps])
['3 <-> y', '2 <-> x', '1 <-> z']
>>> print(['{0} <-> {1}'.format(v, cnf.vpool.obj(v)) for v in cnf.outs])
['5 <-> 6c454aea-c9e1-11e9-bbe3-3af9d34370a9']

from_clauses(clauses)#

This methods copies a list of clauses into a CNF object.

Parameters: clauses (list(list(int))) – a list of clauses

Example:

>>> from pysat.formula import CNF
>>> cnf = CNF(from_clauses=[[-1, 2], [1, -2], [5]])
>>> print(cnf.clauses)
[[-1, 2], [1, -2], [5]]
>>> print(cnf.nv)
5

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

Read a CNF formula from a file in the DIMACS format. A file name is expected as an argument. A default argument is comment_lead for parsing comment lines. A given file can be compressed by either gzip, bzip2, or lzma.

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 pysat.formula import CNF
>>> cnf1 = CNF()
>>> cnf1.from_file('some-file.cnf.gz', compressed_with='gzip')
>>>
>>> cnf2 = CNF(from_file='another-file.cnf')

from_fp(file_pointer, comment_lead=['c'])#

Read a CNF formula from a file pointer. A file pointer should be specified as an argument. The only default argument is comment_lead, which can be used for parsing specific comment lines.

Parameters

file_pointer (file pointer) – a file pointer to read the formula from.
comment_lead (list(str)) – a list of characters leading comment lines

Usage example:

>>> with open('some-file.cnf', 'r') as fp:
...     cnf1 = CNF()
...     cnf1.from_fp(fp)
>>>
>>> with open('another-file.cnf', 'r') as fp:
...     cnf2 = CNF(from_fp=fp)

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

Read a CNF formula from a string. The string should be specified as an argument and should be in the DIMACS CNF 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 DIMACS.
comment_lead (list(str)) – a list of characters leading comment lines

Example:

>>> from pysat.formula import CNF
>>> cnf1 = CNF()
>>> cnf1.from_string('p cnf 2 2\n-1 2 0\n1 -2 0')
>>> print(cnf1.clauses)
[[-1, 2], [1, -2]]
>>>
>>> cnf2 = CNF(from_string='p cnf 3 3\n-1 2 0\n-2 3 0\n-3 0\n')
>>> print(cnf2.clauses)
[[-1, 2], [-2, 3], [-3]]
>>> print(cnf2.nv)
3

negate(topv=None)#

Given a CNF formula \(\mathcal{F}\), this method creates a CNF formula \(\neg{\mathcal{F}}\). The negation of the formula is encoded to CNF with the use of auxiliary Tseitin variables 1. A new CNF 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.

Note that the negation of each clause is encoded with one auxiliary variable if it is not unit size. Otherwise, no auxiliary variable is introduced.

Parameters: topv (int) – top variable identifier if any.
Returns: an object of class CNF.

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

>>> from pysat.formula import CNF
>>> pos = CNF(from_clauses=[[-1, 2], [3]])
>>> neg = pos.negate()
>>> print(neg.clauses)
[[1, -4], [-2, -4], [-1, 2, 4], [4, -3]]
>>> print(neg.auxvars)
[4]
>>> print(neg.enclits)  # literals encoding the negation of clauses
[4, -3]

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

The method can be used to dump a CNF formula into a file pointer in an alien file format, which at this point can either be LP, OPB, or SMT. The file pointer is expected as an argument. Additionally, the target format ‘lp’, ‘opb’, or ‘smt’ may be specified (equal to ‘opb’ by default). Finally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
format (str) – alien file format to use
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import CNF
>>> cnf = CNF()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.lp', 'w') as fp:
...     cnf.to_alien(fp, format='lp')  # writing to the file pointer

to_dimacs()#

Return the current state of the object in DIMACS format.

For example, if ‘some-file.cnf’ contains:

c Example
p cnf 3 3
-1 2 0
-2 3 0
-3 0

Then you can obtain the DIMACS with:

>>> from pysat.formula import CNF
>>> cnf = CNF(from_file='some-file.cnf')
>>> print(cnf.to_dimacs())
c Example
p cnf 3 3
-1 2 0
-2 3 0
-3 0

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

The method is for saving a CNF formula into a file in the DIMACS CNF 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 CNF
>>> cnf = CNF()
...
>>> # the formula is filled with a bunch of clauses
>>> cnf.to_file('some-file-name.cnf')  # writing to a file

to_fp(file_pointer, comments=None)#

The method can be used to save a CNF formula into a file pointer. The file pointer is expected as an argument. Additionally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import CNF
>>> cnf = CNF()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.cnf', 'w') as fp:
...     cnf.to_fp(fp)  # writing to the file pointer

weighted()#

This method creates a weighted copy of the internal formula. As a result, an object of class WCNF is returned. Every clause of the CNF formula is soft in the new WCNF formula and its weight is equal to 1. The set of hard clauses of the formula is empty.

Returns: an object of class WCNF.

Example:

>>> from pysat.formula import CNF
>>> cnf = CNF(from_clauses=[[-1, 2], [3, 4]])
>>>
>>> wcnf = cnf.weighted()
>>> print(wcnf.hard)
[]
>>> print(wcnf.soft)
[[-1, 2], [3, 4]]
>>> print(wcnf.wght)
[1, 1]

class pysat.formula.CNFPlus(from_file=None, from_fp=None, from_string=None, comment_lead=['c'])#

CNF formulas augmented with native cardinality constraints.

This class inherits most of the functionality of the CNF class. The only difference between the two is that CNFPlus supports native cardinality constraints of MiniCard.

The parser of input DIMACS files of CNFPlus assumes the syntax of AtMostK and AtLeastK constraints defined in the description of MiniCard:

c Example: Two cardinality constraints followed by a clause
p cnf+ 7 3
1 -2 3 5 -7 <= 3
4 5 6 -7 >= 2
3 5 7 0

Each AtLeastK constraint is translated into an AtMostK constraint in the standard way: \(\sum_{i=1}^{n}{x_i}\geq k \leftrightarrow \sum_{i=1}^{n}{\neg{x_i}}\leq (n-k)\). Internally, AtMostK constraints are stored in variable atmosts, each being a pair (lits, k), where lits is a list of literals in the sum and k is the upper bound.

Example:

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus(from_string='p cnf+ 7 3\n1 -2 3 5 -7 <= 3\n4 5 6 -7 >= 2\n 3 5 7 0\n')
>>> print(cnf.clauses)
[[3, 5, 7]]
>>> print(cnf.atmosts)
[[[1, -2, 3, 5, -7], 3], [[-4, -5, -6, 7], 2]]
>>> print(cnf.nv)
7

For details on the functionality, see CNF.

append(clause, is_atmost=False)#

Add a single clause or a single AtMostK constraint to CNF+ formula. This method additionally updates the number of variables, i.e. variable self.nv, used in the formula.

If the clause is an AtMostK constraint, this should be set with the use of the additional default argument is_atmost, which is set to False by default.

Parameters

clause (list(int)) – a new clause to add.
is_atmost (bool) – if True, the clause is AtMostK.

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus()
>>> cnf.append([-3, 4])
>>> cnf.append([[1, 2, 3], 1], is_atmost=True)
>>> print(cnf.clauses)
[[-3, 4]]
>>> print(cnf.atmosts)
[[1, 2, 3], 1]

copy()#

This method can be used for creating a copy of a CNFPlus object. It creates another object of the CNFPlus class, call the copy function of CNF class and makes use of the deepcopy functionality to copy the atmost constraints.

Returns: an object of class CNFPlus.

Example:

>>> cnf1 = CNFPlus()
>>> cnf1.extend([[-1, 2], [1]])
>>> cnf1.append([[1, 2], 1], is_atmost=True)
>>> cnf2 = cnf1.copy()
>>> print(cnf2.clauses)
[[-1, 2], [1]]
>>> print(cnf2.nv)
2
>>> print(cnf2.atmosts)
[[[1, 2], 1]]

extend(formula)#

Extend the CNF+ formula with more clauses and/or AtMostK constraints. The additional clauses and AtMostK constraints to add should be given in the form of CNFPlus. Alternatively, a list of clauses can be added too. For every single clause and AtMostK constraint in the input formula, method append() is invoked.

Parameters: formula (CNFPlus) – new constraints to add.

Example:

>>> from pysat.formula import CNFPlus
>>> cnf1 = CNFPlus()
>>> cnf1.extend([[-3, 4], [5, 6], [[1, 2, 3], 1]])
>>> print(cnf1.clauses)
[[-3, 4], [5, 6]]
>>> print(cnf1.atmosts)
[[[1, 2, 3], 1]]
>>> cnf2 = CNFPlus()
>>> cnf2.extend(cnf1)
>>> print(cnf1.clauses)
[[-3, 4], [5, 6]]
>>> print(cnf1.atmosts)
[[[1, 2, 3], 1]]

from_fp(file_pointer, comment_lead=['c'])#

Read a CNF+ formula from a file pointer. A file pointer should be specified as an argument. The only default argument is comment_lead, which can be used for parsing specific comment lines.

Parameters

file_pointer (file pointer) – a file pointer to read the formula from.
comment_lead (list(str)) – a list of characters leading comment lines

Usage example:

>>> with open('some-file.cnf+', 'r') as fp:
...     cnf1 = CNFPlus()
...     cnf1.from_fp(fp)
>>>
>>> with open('another-file.cnf+', 'r') as fp:
...     cnf2 = CNFPlus(from_fp=fp)

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

The method can be used to dump a CNF+ formula into a file pointer in an alien file format, which at this point can either be LP, OPB, or SMT. The file pointer is expected as an argument. Additionally, the target format ‘lp’, ‘opb’, or ‘smt’ may be specified (equal to ‘opb’ by default). Finally, supplementary comment lines can be specified in the comments parameter.

Note

SMT-LIB2 does not directly support PB constraints. As a result, native cardinality constraints of CNF+ cannot be translated to SMT-LIB2 unless an explicit cardinality encoding is applied. You may want to use Z3’s API instead (see its PB interface).

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
format (str) – alien file format to use
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.lp', 'w') as fp:
...     cnf.to_alien(fp, format='lp')  # writing to the file pointer

to_dimacs()#

Return the current state of the object in extended DIMACS format.

For example, if ‘some-file.cnf’ contains:

c Example
p cnf+ 7 3
1 -2 3 5 -7 <= 3
4 5 6 -7 >= 2
3 5 7 0

Then you can obtain the DIMACS with:

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus(from_file='some-file.cnf')
>>> print(cnf.to_dimacs())
c Example
p cnf+ 7 3
3 5 7 0
1 -2 3 5 -7 <= 3
-4 -5 -6 7 <= 2

to_fp(file_pointer, comments=None)#

The method can be used to save a CNF+ formula into a file pointer. The file pointer is expected as an argument. Additionally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.cnf+', 'w') as fp:
...     cnf.to_fp(fp)  # writing to the file pointer

weighted()#

This method creates a weighted copy of the internal formula. As a result, an object of class WCNFPlus is returned. Every clause of the CNFPlus formula is soft in the new WCNFPlus formula and its weight is equal to 1. The set of hard clauses of the new formula is empty. The set of cardinality constraints remains unchanged.

Returns: an object of class WCNFPlus.

Example:

>>> from pysat.formula import CNFPlus
>>> cnf = CNFPlus()
>>> cnf.append([-1, 2])
>>> cnf.append([3, 4])
>>> cnf.append([[1, 2], 1], is_atmost=True)
>>>
>>> wcnf = cnf.weighted()
>>> print(wcnf.hard)
[]
>>> print(wcnf.soft)
[[-1, 2], [3, 4]]
>>> print(wcnf.wght)
[1, 1]
>>> print(wcnf.atms)
[[[1, 2], 1]]

class pysat.formula.IDPool(start_from=1, occupied=[])#

A simple manager of variable IDs. It can be used as a pool of integers assigning an ID to any object. Identifiers are to start from 1 by default. The list of occupied intervals is empty be default. If necessary the top variable ID can be accessed directly using the top variable.

Parameters

start_from (int) – the smallest ID to assign.
occupied (list(list(int))) – a list of occupied intervals.

id(obj=None)#

The method is to be used to assign an integer variable ID for a given new object. If the object already has an ID, no new ID is created and the old one is returned instead.

An object can be anything. In some cases it is convenient to use string variable names. Note that if the object is not provided, the method will return a new id unassigned to any object.

Parameters: obj – an object to assign an ID to.
Return type: int.

Example:

>>> from pysat.formula import IDPool
>>> vpool = IDPool(occupied=[[12, 18], [3, 10]])
>>>
>>> # creating 5 unique variables for the following strings
>>> for i in range(5):
...    print(vpool.id('v{0}'.format(i + 1)))
1
2
11
19
20

In some cases, it makes sense to create an external function for accessing IDPool, e.g.:

>>> # continuing the previous example
>>> var = lambda i: vpool.id('var{0}'.format(i))
>>> var(5)
20
>>> var('hello_world!')
21

obj(vid)#

The method can be used to map back a given variable identifier to the original object labeled by the identifier.

Parameters: vid (int) – variable identifier.
Returns: an object corresponding to the given identifier.

Example:

>>> vpool.obj(21)
'hello_world!'

occupy(start, stop)#

Mark a given interval as occupied so that the manager could skip the values from start to stop (inclusive).

Parameters

start (int) – beginning of the interval.
stop (int) – end of the interval.

restart(start_from=1, occupied=[])#: Restart the manager from scratch. The arguments replicate those of the constructor of IDPool.

class pysat.formula.WCNF(from_file=None, from_fp=None, from_string=None, comment_lead=['c'])#

Class for manipulating partial (weighted) CNF formulas. It can be used for creating formulas, reading them from a file, or writing them to a file. The comment_lead parameter can be helpful when one needs to parse specific comment lines starting not with character c but with another character or a string.

Parameters

from_file (str) – a DIMACS CNF filename to read from
from_fp (file_pointer) – a file pointer to read from
from_string (str) – a string storing a CNF formula
comment_lead (list(str)) – a list of characters leading comment lines

append(clause, weight=None)#

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

The clause can be hard or soft depending on the weight argument. If no weight is set, the clause is considered to be hard.

Parameters

clause (list(int)) – a new clause to add.
weight (integer or None) – integer weight of the clause.

>>> from pysat.formula import WCNF
>>> cnf = WCNF()
>>> cnf.append([-1, 2])
>>> cnf.append([1], weight=10)
>>> cnf.append([-2], weight=20)
>>> print(cnf.hard)
[[-1, 2]]
>>> print(cnf.soft)
[[1], [-2]]
>>> print(cnf.wght)
[10, 20]

copy()#

This method can be used for creating a copy of a WCNF object. It creates another object of the WCNF class and makes use of the deepcopy functionality to copy both hard and soft clauses.

Returns: an object of class WCNF.

Example:

>>> cnf1 = WCNF()
>>> cnf1.append([-1, 2])
>>> cnf1.append([1], weight=10)
>>>
>>> cnf2 = cnf1.copy()
>>> print(cnf2.hard)
[[-1, 2]]
>>> print(cnf2.soft)
[[1]]
>>> print(cnf2.wght)
[10]
>>> print(cnf2.nv)
2

extend(clauses, weights=None)#

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

The clauses can be hard or soft depending on the weights argument. If no weights are set, the clauses are considered to be hard.

Parameters

clauses (list(list(int))) – a list of new clauses to add.
weights (list(int)) – a list of integer weights.

Example:

>>> from pysat.formula import WCNF
>>> cnf = WCNF()
>>> cnf.extend([[-3, 4], [5, 6]])
>>> cnf.extend([[3], [-4], [-5], [-6]], weights=[1, 5, 3, 4])
>>> print(cnf.hard)
[[-3, 4], [5, 6]]
>>> print(cnf.soft)
[[3], [-4], [-5], [-6]]
>>> print(cnf.wght)
[1, 5, 3, 4]

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

Read a WCNF formula from a file in the DIMACS format. A file name is expected as an argument. A default argument is comment_lead for parsing comment lines. A given file can be compressed by either gzip, bzip2, or lzma.

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

Usage example:

>>> from pysat.formula import WCNF
>>> cnf1 = WCNF()
>>> cnf1.from_file('some-file.wcnf.bz2', compressed_with='bzip2')
>>>
>>> cnf2 = WCNF(from_file='another-file.wcnf')

from_fp(file_pointer, comment_lead=['c'])#

Read a WCNF formula from a file pointer. A file pointer should be specified as an argument. The only default argument is comment_lead, which can be used for parsing specific comment lines.

Parameters

file_pointer (file pointer) – a file pointer to read the formula from.
comment_lead (list(str)) – a list of characters leading comment lines

Usage example:

>>> with open('some-file.cnf', 'r') as fp:
...     cnf1 = WCNF()
...     cnf1.from_fp(fp)
>>>
>>> with open('another-file.cnf', 'r') as fp:
...     cnf2 = WCNF(from_fp=fp)

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

Read a WCNF formula from a string. The string should be specified as an argument and should be in the DIMACS CNF 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 DIMACS.
comment_lead (list(str)) – a list of characters leading comment lines

Example:

>>> from pysat.formula import WCNF
>>> cnf1 = WCNF()
>>> cnf1.from_string('p wcnf 2 2 2\n 2 -1 2 0\n1 1 -2 0')
>>> print(cnf1.hard)
[[-1, 2]]
>>> print(cnf1.soft)
[[1, 2]]
>>>
>>> cnf2 = WCNF(from_string='p wcnf 3 3 2\n2 -1 2 0\n2 -2 3 0\n1 -3 0\n')
>>> print(cnf2.hard)
[[-1, 2], [-2, 3]]
>>> print(cnf2.soft)
[[-3]]
>>> print(cnf2.nv)
3

normalize_negatives(negatives)#

Iterate over all soft clauses with negative weights and add their negation either as a hard clause or a soft one.

Parameters: negatives (list(list(int))) – soft clauses with their negative weights.

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

The method can be used to dump a WCNF formula into a file pointer in an alien file format, which at this point can either be LP, OPB, or SMT. The file pointer is expected as an argument. Additionally, the target format ‘lp’, ‘opb’, or ‘smt’ may be specified (equal to ‘opb’ by default). Finally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
format (str) – alien file format to use
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import WCNF
>>> cnf = WCNF()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.lp', 'w') as fp:
...     cnf.to_alien(fp, format='lp')  # writing to the file pointer

to_dimacs()#

Return the current state of the object in extended DIMACS format.

For example, if ‘some-file.cnf’ contains:

c Example
p wcnf 2 3 10
1 -1 0
2 -2 0
10 1 2 0

Then you can obtain the DIMACS with:

>>> from pysat.formula import WCNF
>>> cnf = WCNF(from_file='some-file.cnf')
>>> print(cnf.to_dimacs())
c Example
p wcnf 2 3 10
10 1 2 0
1 -1 0
2 -2 0

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

The method is for saving a WCNF formula into a file in the DIMACS CNF 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

Example:

>>> from pysat.formula import WCNF
>>> wcnf = WCNF()
...
>>> # the formula is filled with a bunch of clauses
>>> wcnf.to_file('some-file-name.wcnf')  # writing to a file

to_fp(file_pointer, comments=None)#

The method can be used to save a WCNF formula into a file pointer. The file pointer is expected as an argument. Additionally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import WCNF
>>> wcnf = WCNF()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.wcnf', 'w') as fp:
...     wcnf.to_fp(fp)  # writing to the file pointer

unweighted()#

This method creates a plain (unweighted) copy of the internal formula. As a result, an object of class CNF is returned. Every clause (both hard or soft) of the WCNF formula is copied to the clauses variable of the resulting plain formula, i.e. all weights are discarded.

Returns: an object of class CNF.

Example:

>>> from pysat.formula import WCNF
>>> wcnf = WCNF()
>>> wcnf.extend([[-3, 4], [5, 6]])
>>> wcnf.extend([[3], [-4], [-5], [-6]], weights=[1, 5, 3, 4])
>>>
>>> cnf = wcnf.unweighted()
>>> print(cnf.clauses)
[[-3, 4], [5, 6], [3], [-4], [-5], [-6]]

class pysat.formula.WCNFPlus(from_file=None, from_fp=None, from_string=None, comment_lead=['c'])#

WCNF formulas augmented with native cardinality constraints.

This class inherits most of the functionality of the WCNF class. The only difference between the two is that WCNFPlus supports native cardinality constraints of MiniCard.

The parser of input DIMACS files of WCNFPlus assumes the syntax of AtMostK and AtLeastK constraints following the one defined for CNFPlus in the description of MiniCard:

c Example: Two (hard) cardinality constraints followed by a soft clause
p wcnf+ 7 3 10
10 1 -2 3 5 -7 <= 3
10 4 5 6 -7 >= 2
5 3 5 7 0

Note that every cardinality constraint is assumed to be hard, i.e. soft cardinality constraints are currently not supported.

Each AtLeastK constraint is translated into an AtMostK constraint in the standard way: \(\sum_{i=1}^{n}{x_i}\geq k \leftrightarrow \sum_{i=1}^{n}{\neg{x_i}}\leq (n-k)\). Internally, AtMostK constraints are stored in variable atms, each being a pair (lits, k), where lits is a list of literals in the sum and k is the upper bound.

Example:

>>> from pysat.formula import WCNFPlus
>>> cnf = WCNFPlus(from_string='p wcnf+ 7 3 10\n10 1 -2 3 5 -7 <= 3\n10 4 5 6 -7 >= 2\n5 3 5 7 0\n')
>>> print(cnf.soft)
[[3, 5, 7]]
>>> print(cnf.wght)
[5]
>>> print(cnf.hard)
[]
>>> print(cnf.atms)
[[[1, -2, 3, 5, -7], 3], [[-4, -5, -6, 7], 2]]
>>> print(cnf.nv)
7

For details on the functionality, see WCNF.

append(clause, weight=None, is_atmost=False)#

Add a single clause or a single AtMostK constraint to WCNF+ formula. This method additionally updates the number of variables, i.e. variable self.nv, used in the formula.

If the clause is an AtMostK constraint, this should be set with the use of the additional default argument is_atmost, which is set to False by default.

If is_atmost is set to False, the clause can be either hard or soft depending on the weight argument. If no weight is specified, the clause is considered hard. Otherwise, the clause is soft.

Parameters

clause (list(int)) – a new clause to add.
weight (integer or None) – an integer weight of the clause.
is_atmost (bool) – if True, the clause is AtMostK.

>>> from pysat.formula import WCNFPlus
>>> cnf = WCNFPlus()
>>> cnf.append([-3, 4])
>>> cnf.append([[1, 2, 3], 1], is_atmost=True)
>>> cnf.append([-1, -2], weight=35)
>>> print(cnf.hard)
[[-3, 4]]
>>> print(cnf.atms)
[[1, 2, 3], 1]
>>> print(cnf.soft)
[[-1, -2]]
>>> print(cnf.wght)
[35]

copy()#

This method can be used for creating a copy of a WCNFPlus object. It creates another object of the WCNFPlus class, call the copy function of WCNF class and makes use of the deepcopy functionality to copy the atmost constraints.

Returns: an object of class WCNFPlus.

Example:

>>> cnf1 = WCNFPlus()
>>> cnf1.append([-1, 2])
>>> cnf1.append([1], weight=10)
>>> cnf1.append([[1, 2], 1], is_atmost=True)
>>> cnf2 = cnf1.copy()
>>> print(cnf2.hard)
[[-1, 2]]
>>> print(cnf2.soft)
[[1]]
>>> print(cnf2.wght)
[10]
>>> print(cnf2.nv)
2
>> print(cnf2.atms)
[[[1, 2], 1]]

from_fp(file_pointer, comment_lead=['c'])#

Read a WCNF+ formula from a file pointer. A file pointer should be specified as an argument. The only default argument is comment_lead, which can be used for parsing specific comment lines.

Parameters

file_pointer (file pointer) – a file pointer to read the formula from.
comment_lead (list(str)) – a list of characters leading comment lines

Usage example:

>>> with open('some-file.wcnf+', 'r') as fp:
...     cnf1 = WCNFPlus()
...     cnf1.from_fp(fp)
>>>
>>> with open('another-file.wcnf+', 'r') as fp:
...     cnf2 = WCNFPlus(from_fp=fp)

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

The method can be used to dump a WCNF+ formula into a file pointer in an alien file format, which at this point can either be LP, OPB, or SMT. The file pointer is expected as an argument. Additionally, the target format ‘lp’, ‘opb’, or ‘smt’ may be specified (equal to ‘opb’ by default). Finally, supplementary comment lines can be specified in the comments parameter.

Note

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
format (str) – alien file format to use
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import WCNFPlus
>>> cnf = WCNFPlus()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.lp', 'w') as fp:
...     cnf.to_alien(fp, format='lp')  # writing to the file pointer

to_dimacs()#

Return the current state of the object in extended DIMACS format.

For example, if ‘some-file.cnf’ contains:

c Example
p wcnf+ 7 3 10
10 1 -2 3 5 -7 <= 3
10 4 5 6 -7 >= 2
5 3 5 7 0

Then you can obtain the DIMACS with:

>>> from pysat.formula import WCNFPlus
>>> cnf = WCNFPlus(from_file='some-file.cnf')
>>> print(cnf.to_dimacs())
c Example
p wcnf+ 7 4 10
10 -1 3 5 0
5 3 5 7 0
10 1 -2 3 5 -7 <= 3
10 -4 -5 -6 7 <= 2

to_fp(file_pointer, comments=None)#

The method can be used to save a WCNF+ formula into a file pointer. The file pointer is expected as an argument. Additionally, supplementary comment lines can be specified in the comments parameter.

Parameters

file_pointer (file pointer) – a file pointer where to store the formula.
comments (list(str)) – additional comments to put in the file.

Example:

>>> from pysat.formula import WCNFPlus
>>> cnf = WCNFPlus()
...
>>> # the formula is filled with a bunch of clauses
>>> with open('some-file.wcnf+', 'w') as fp:
...     cnf.to_fp(fp)  # writing to the file pointer

unweighted()#

This method creates a plain (unweighted) copy of the internal formula. As a result, an object of class CNFPlus is returned. Every clause (both hard or soft) of the original WCNFPlus formula is copied to the clauses variable of the resulting plain formula, i.e. all weights are discarded.

Note that the cardinality constraints of the original (weighted) formula remain unchanged in the new (plain) formula.

Returns: an object of class CNFPlus.

Example:

>>> from pysat.formula import WCNF
>>> wcnf = WCNFPlus()
>>> wcnf.extend([[-3, 4], [5, 6]])
>>> wcnf.extend([[3], [-4], [-5], [-6]], weights=[1, 5, 3, 4])
>>> wcnf.append([[1, 2, 3], 1], is_atmost=True)
>>>
>>> cnf = wcnf.unweighted()
>>> print(cnf.clauses)
[[-3, 4], [5, 6], [3], [-4], [-5], [-6]]
>>> print(cnf.atmosts)
[[[1, 2, 3], 1]]

Cardinality encodings (pysat.card)

Pseudo-Boolean encodings (pysat.pb)

Boolean formula manipulation (pysat.formula)#

List of classes#

Module description#

Module details#

Boolean formula manipulation (`pysat.formula`)#