Boolean formula manipulation (`pysat.formula`)#

List of classes#

`IDPool`	A simple manager of variable IDs.
`Formula`	Abstract formula class.
`Atom`	Atomic formula, i.e. a variable or constant.
`And`	Conjunction.
`Or`	Disjunction.
`Neg`	Negation.
`Implies`	Implication.
`Equals`	Equivalence.
`XOr`	Exclusive disjunction.
`ITE`	If-then-else operator.
`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. The toolkit implements several facilities to manupulate Boolean formulas. Namely, one can opt for creating arbitrary non-clausal formulas suitable for simple problem encodings requiring no or little knowledge about the process of logical encoding. However, the main and most often used kind of formula in PySAT is represented by the CNF class, which can be used to define 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.

Apart from the aforementioned variants of (W)CNF formulas, the module now offers a few additional classes for managing non-clausal Boolean formulas. Namely, a user may create complex formulas using variables (atomic formulas implemented as objects of class Atom), and the following logic connectives: And, Or, Neg, Implies, Equals, XOr, and ITE. (All of these classes inherit from the base class Formula.) Arbitrary combinations of these logic connectives are allowed. Importantly, the module provides seamless integration of CNF and various subclasses of Formula with the possibility to clausify these on demand.

>>> from pysat.formula import *
>>> from pysat.solvers import Solver

# creating two formulas: CNF and XOr
>>> cnf = CNF(from_clauses=[[-1, 2], [-2, 3]])
>>> xor = Atom(1) ^ Atom(2) ^ Atom(4)

# passing the conjunction of these to the solver
>>> with Solver(bootstrap_with=xor & cnf) as solver:
...    # setting Atom(3) to false results in only one model
...    for model in solver.enum_models(assumptions=Formula.literals([~Atom(3)])):
...        print(Formula.formulas(model, atoms_only=True))  # translating the model back to atoms
>>>
[Neg(Atom(1)), Neg(Atom(2)), Neg(Atom(3)), Atom(4)]

Note

Combining CNF formulas with non-CNF ones will not necessarily result in the best possible encoding of the complex formula. The on-the-fly encoder may introduce variables that a human would avoid using, e.g. if cnf1 and cnf2 are CNF formulas then And(cnf1, cnf2) will introduce auxiliary variables v1 and v2 encoding them, respectively (although it is enough to join their sets of clauses).

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.And(*args, **kwargs)#

Conjunction. Given a list of operands (subformulas) \(f_i\), \(i \in \{1,\ldots,n\}, n \in \mathbb{N}\), it creates a formula \(\bigwedge_{i=1}^{n}{f_i}\). The list of operands of size at least 1 should be passed as arguments to the constructor.

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> conj = And(x, y, z)

If an additional Boolean keyword argument merge is provided set to True, the toolkit will try to flatten the current And formula merging its conjuctive sub-operands into the list of operands. For example, if And(And(x, y), z, merge=True) is called, a new Formula object will be created with two operands: And(x, y) and z, followed by merging x and y into the list of root-level And. This will result in a formula And(x, y, z). Merging sub-operands is enabled by default if bitwise operations are used to create And formulas.

Example:

>>> from pysat.formula import *
>>> a1 = And(And(Atom('x'), Atom('y')), Atom('z'))
>>> a2 = And(And(Atom('x'), Atom('y')), Atom('z'), merge=True)
>>> a3 = Atom('x') & Atom('y') & Atom('z')
>>>
>>> repr(a1)
"And[And[Atom('x'), Atom('y')], Atom('z')]"
>>> repr(a2)
"And[Atom('x'), Atom('y'), Atom('z')]"
>>> repr(a2)
"And[Atom('x'), Atom('y'), Atom('z')]"
>>>
>>> id(a1) == id(a2)
False
>>>
>>> id(a2) == id(a3)
True  # formulas a2 and a3 refer to the same object

Note

If there are two formulas representing the same fact with and without merging enabled, they technically sit in two distinct objects. Although PySAT tries to avoid it, clausification of these two formulas may result in unique (different) auxiliary variables assigned to such two formulas.

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformulas and creates a new formula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = x & y & z
>>>
>>> print(a.simplified(assumptions=[y]))
x & z
>>> print(a.simplified(assumptions=[~y]))
F  # False

class pysat.formula.Atom(*args, **kwargs)#

Atomic formula, i.e. a variable or constant. Although we often refer to negated literals as atomic formulas too, they are techically implemented as Neg(Atom).

To create an atomic formula, a user needs to specify an object this formula should signify. When it comes to clausifying the formulas this atom is involved in, the atom receives an auxiliary variable assigned to it as a name.

Example:

>>> from pysat.formula import *
>>> x = Atom('x')
>>> y = Atom(object='y')
>>> # checking x's name
>>> x.name
>>> # None
>>> # right, that's because the atom is not yet clausified
>>> x.clausify()
>>> x.name
1

If a given object is a positive integer (negative integers aren’t allowed), the integer itself serves as the atom’s name, which is assigned in the constructor, i.e. no call to clausify() is required.

Example:

>>> from pysat.formula import Atom
>>> x, y = Atom(1), Atom(2)
>>> x.name
1
>>> y.name
2

Special atoms are reserved for the Boolean constants True and False. Namely, Atom(False) and Atom(True) can be accessed through the constants PYSAT_FALSE and PYSAT_TRUE, respectively.

Example:

>>> from pysat.formula import *
>>>
>>> print(PYSAT_TRUE, repr(PYSAT_TRUE))
T Atom(True)
>>>
>>> print(PYSAT_FALSE, repr(PYSAT_FALSE))
F Atom(False)

Note

Constant Atom(True) is distinguished from variable Atom(1) by checking the type of the object (bool vs int).

simplified(assumptions=[])#

Checks if the current literal appears in the list of assumptions provided in argument assumptions. If it is, the method returns PYSAT_TRUE. If the opposite atom is present in assumptions, the method returns PYSAT_FALSE. Otherwise, it return self.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: PYSAT_TRUE, PYSAT_FALSE, or self

class pysat.formula.CNF(*args, **kwargs)#

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
by_ref (bool) – flag to indicate how to copy clauses - by reference or deep-copy

append(clause, update_vpool=False)#

Add one more clause to CNF 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 CNF 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 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, by_ref=False)#

This methods copies a list of clauses into a CNF object. The optional keyword argument by_ref, which is by default set to False, signifies whether the clauses should be deep-copied or copied by reference (by default, deep-copying is applied although it is slower).

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

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

simplified(assumptions=[])#: As any other Formula type, CNF formulas have this method, although intentionally left unimplemented. Raises a FormulaError exception.

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(*args, **kwargs)#

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

Additionally, CNFPlus support pseudo-Boolean constraints, i.e. weighted linear constraints by extending the above format. Basically, a pseudo-Boolean constraint needs to specify all the summands as weight*literal with the entire constraint being prepended with character w as follows:

c Example: One cardinality constraint and one PB constraint followed by a clause
p cnf+ 7 3
1 -2 3 5 -7 <= 3
w 1*4 2*5 1*6 3*-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.Equals(*args, **kwargs)#

Equivalence. Given a list of operands (subformulas) \(f_i\), \(i \in \{1,\ldots,n\}, n \in \mathbb{N}\), it creates a formula \(f_1 \leftrightarrow f_2 \leftrightarrow\ldots\leftrightarrow f_n\). The list of operands of size at least 2 should be passed as arguments to the constructor.

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> equiv = Equals(x, y, z)

If an additional Boolean keyword argument merge is provided set to True, the toolkit will try to flatten the current Equals formula merging its equivalence sub-operands into the list of operands. For example, if Equals(Equals(x, y), z, merge=True) is called, a new Formula object will be created with two operands: Equals(x, y) and z, followed by merging x and y into the list of root-level Equals. This will result in a formula Equals(x, y, z). Merging sub-operands is enabled by default if bitwise operations are used to create Equals formulas.

Example:

>>> from pysat.formula import *
>>> a1 = Equals(Equals(Atom('x'), Atom('y')), Atom('z'))
>>> a2 = Equals(Equals(Atom('x'), Atom('y')), Atom('z'), merge=True)
>>> a3 = Atom('x') == Atom('y') == Atom('z')
>>>
>>> print(a1)
(x @ y) @ z
>>> print(a2)
x @ y @ z
>>> print(a3)
x @ y @ z
>>>
>>> id(a1) == id(a2)
False
>>>
>>> id(a2) == id(a3)
True  # formulas a2 and a3 refer to the same object

Note

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformulas and creates a new formula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = x @ y @ z
>>>
>>> print(a.simplified(assumptions=[y]))
x & z    # x and z must also be True
>>> print(a.simplified(assumptions=[~y]))
~x & ~z  # x and z must also be False

class pysat.formula.Formula(*args, **kwargs)#

Abstract formula class. At the same time, the class is a factory for its children and can be used this way although it is recommended to create objects of the children classes directly. In particular, its children classes include Atom (atomic formulas - variables and constants), Neg (negations), And (conjunctions), Or (disjunctions), Implies (implications), Equals (equalities), XOr (exclusive disjunctions), and ITE (if-then-else operations).

Due to the need to clausify formulas, an object of any subclass of Formula is meant to be represented in memory by a single copy. This is achieved by storing a dictionary of all the known formulas attached to a given context. Thus, once a particular context is activated, its dictionary will make sure each formula variable refers to a single representation of the formula object it aims to refer. When it comes to clausifying this formula, the formula is encoded exactly once, despite it may be potentially used multiple times as part of one of more complex formulas.

Example:

>>> from pysat.formula import *
>>>
>>> x1, x2 = Atom('x'), Atom('x')
>>> id(x1) == id(x2)
True  # x1 and x2 refer to the same atom
>>> id(x1 & Atom('y')) == id(Atom('y') & x2)
True  # it holds if constructing complex formulas with them as subformulas

The class supports multi-context operation. A user may have formulas created and clausified in different context. They can also switch from one context to another and/or cleanup the instances known in some or all contexts.

Example:

>>> from pysat.formula import *
>>> f1 = Or(And(...))  # arbitrary formula
>>> # by default, the context is set to 'default'
>>> # another context can be created like this:
>>> Formula.set_context(context='some-other-context')
>>> # the new context knows nothing about formula f1
>>> # ...
>>> # cleaning up context 'some-other-context'
>>> # this deletes all the formulas known in this context
>>> Formula.cleanup(context='some-other-context')
>>> # switching back to 'default'
>>> Formula.set_context(context='default')

A user may also want to disable duplicate blocking, which can be achieved by setting the context to None.

Boolean constants False and True are represented by the atomic “formulas” Atom(False) and Atom(True), respectively. There are two constants storing these values: PYSAT_FALSE and PYSAT_TRUE.

>>> PYSAT_FALSE, PYSAT_TRUE
(Atom(False), Atom(True))

static attach_vpool(vpool, context='default')#

Attach an external IDPool to be associated with a given context. This is useful when a user has an already created IDPool object and wants to reuse it when clausifying their Formula objects.

Parameters:

vpool (IDPool) – an external variable manager
context (hashable) – target context to be the user of the vpool

clausify()#

This method applies Tseitin transformation to the formula. Recursively gives all the formulas Boolean names accordingly and uses them in the current logic connective following its semantics. As a result, each subformula stores its clausal representation independently of other subformulas (and independently of the root formula).

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = (x @ y) | z
>>>
>>> a.clausify()  # clausifying formula a
>>>
>>> # let's what clauses represent the root logic connective
>>> a.clauses
[[3, 4]]  # 4 corresponds to z while 3 represents the equality x @ y

static cleanup(context=None)#

Clean up either a given context (if specified as different from None) or all contexts (otherwise); afterwards, start the “default” context from scratch.

A context is cleaned by destroying all the associated Formula objects and all the corresponding variable managers. This may be useful if a user wants to start encoding their problem from scratch.

Note

Once cleaning of a context is done, the objects referring to the context’s formulas must not be used. At this point, they are orphaned and can’t get re-clausified.

Parameters:: context (None or hashable) – target context

static export_vpool(active=True, context='default')#

Opposite to attach_vpool(), this method returns a variable managed attached to a given context, which may be useful for external use.

Parameters:

active (bool) – export the currently active context
context (hashable) – context using the vpool we are interested in (if active is False)

Return type:

IDPool

static formulas(lits, atoms_only=True)#

Given a list of integer literal identifiers, this method returns a list of formulas corresponding to these identifiers. Basically, the method can be seen as mapping auxiliary variables naming formulas to the corresponding formulas they name.

If the argument atoms_only is set to True only, the method will return a subset of formulas, including only atomic formulas (literals). Otherwise, any formula whose name occurs in the input list will be included in the result.

Parameters:

lits (iterable) – input list of literals
atoms_only (bool) – include all known formulas or atomic ones only

Return type:

list(Formula)

Example:

>>> from pysat.formula import *
>>> from pysat.solvers import Solver
>>>
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = (x @ y) ^ z
>>>
>>> with Solver(bootstrap_with=a) as solver:
...     for model in solver.enum_models():
...         # using method formulas to map the model back to atoms
...         print(Formula.formulas(model, atoms_only=True))
...
[Neg(Atom('x')), Neg(Atom('y')), Neg(Atom('z'))]
[Neg(Atom('x')), Atom('y'), Atom('z')]
[Atom('x'), Atom('y'), Neg(Atom('z'))]
[Atom('x'), Neg(Atom('y')), Atom('z')]

static literals(forms)#

Extract formula names for a given list of formulas and return them as a list of integer identifiers. Essentially, the method is the opposite to formulas().

Parameters:: forms (iterable) – list of formulas to map
Return type:: list(int)

Example:

>>> from pysat.solvers import Solver
>>> from pysat.formula import *
>>>
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = (x @ y) ^ z
>>>
>>> # applying Tseitin transformation to formula a
>>> a.clausify()
>>>
>>> # checking what facts the internal vpool knows
>>> print(Formula.export_vpool().id2obj)
{1: Atom('x'), 2: Atom('y'), 3: Equals[Atom('x'), Atom('y')], 4: Atom('z')}
>>>
>>> # now, mapping two atoms to their integer id representations
>>> Formula.literals(forms=[Atom('x'), ~Atom('z')])
[1, -4]

satisfied(model)#

Given a list of atomic formulas, this method checks whether the current formula is satisfied by assigning these atoms. The method returns True if the formula gets satisfied, False if it is falsified, and None if the answer is unknown.

Parameters:: model (list(Formula)) – list of atomic formulas
Return type:: bool or None

Example:

>>> from pysat.formula import *
>>>
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = (x @ y) | z
>>>
>>> a.satisfied(model=[z])
True
>>> a.satisfied(model=[~z])
>>> # None, as it is not enough to set ~z to determine satisfiability of a

static set_context(context='default')#

Set the current context of interest. If set to None, no context will be assumed and duplicate checking will be disabled as a result.

Parameters:: context (hashable) – new active context

simplified(assumptions=[])#

Given a list of assumption atomic formula literals, this method recursively assigns these atoms to the corresponding values followed by formula simplification. As a result, a new formula object is returned.

Parameters:: assumptions (list) – atomic formula objects
Return type:: Formula

Example:

>>> from pysat.formula import *
>>>
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = (x @ y) | z  # a formula over 3 variables: x, y, and z
>>>
>>> a.simplified(assumptions=[z])
Atom(True)
>>>
>>> a.simplified(assumptions=[~z])
Equals[Atom('x'), Atom('y')]
>>>
>>> b = a ^ Atom('p')  # a more complex formula
>>>
>>> b.simplified(assumptions=[x, ~Atom('p')])
Or[Atom('y'), Atom('z')]

exception pysat.formula.FormulaError#: This exception is raised when an formula-related issue occurs.

class pysat.formula.FormulaType(value)#

This class represents a C-like enum type for choosing the formula type to use. The values denoting all the formula types are as follows:

ATOM = 0
AND = 1
OR = 2
NEG = 3
IMPL = 4
EQ = 5
XOR = 6
ITE = 7

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.ITE(*args, **kwargs)#

If-then-else operator. Given three operands (subformulas) \(x\), \(y\), and \(z\), it creates a formula \((x \rightarrow y) \land (\neg{x} \rightarrow z)\). The operands should be passed as arguments to the constructor.

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> ite = ITE(x, y, z)
>>>
>>> print(ite)
>>> (x >> y) & (~x >> z)

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformulas and creates a new formula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> ite = ITE(x, y, z)
>>>
>>> print(ite.simplified(assumptions=[y]))
x | z
>>> print(ite.simplified(assumptions=[~y]))
~x & z

class pysat.formula.Implies(*args, **kwargs)#

Implication. Given two operands \(f_1\) and \(f_2\), it creates a formula \(f_1 \rightarrow f_2\). The operands must be passed to the constructors either as two arguments or two keyword arguments left and right.

Example:

>>> from pysat.formula import *
>>> x, y = Atom('x'), Atom('y')
>>> a = Implies(x, y)
>>> print(a)
x >> y

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the left and right subformulas and then creates and returns a new formula with these simplified subformulas.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y')
>>> a = x >> y
>>>
>>> print(a.simplified(assumptions=[y]))
T
>>> print(a.simplified(assumptions=[~y]))
~x

class pysat.formula.Neg(*args, **kwargs)#

Negation. Given a single operand (subformula) \(f\), it creates a formula \(\neg{f}\). The operand must be passed as an argument to the constructor.

Example:

>>> from pysat.formula import *
>>> x = Atom('x')
>>> n1 = Neg(x)
>>> n2 = Neg(subformula=x)
>>> print(n1, n2)
~x, ~x
>>> n3 = ~n1
>>> print(n3)
x

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformula and then creates and returns a new formula with this simplified subformula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = x & y | z
>>> b = ~a
>>>
>>> print(b.simplified(assumptions=[y]))
~(x | z)
>>> print(b.simplified(assumptions=[~y]))
~z

class pysat.formula.Or(*args, **kwargs)#

Disjunction. Given a list of operands (subformulas) \(f_i\), \(i \in \{1,\ldots,n\}, n \in \mathbb{N}\), it creates a formula \(\bigvee_{i=1}^{n}{f_i}\). The list of operands of size at least 1 should be passed as arguments to the constructor.

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> conj = Or(x, y, z)

If an additional Boolean keyword argument merge is provided set to True, the toolkit will try to flatten the current Or formula merging its conjuctive sub-operands into the list of operands. For example, if Or(Or(x, y), z, merge=True) is called, a new Formula object will be created with two operands: Or(x, y) and z, followed by merging x and y into the list of root-level Or. This will result in a formula Or(x, y, z). Merging sub-operands is enabled by default if bitwise operations are used to create Or formulas.

Example:

>>> from pysat.formula import *
>>> a1 = Or(Or(Atom('x'), Atom('y')), Atom('z'))
>>> a2 = Or(Or(Atom('x'), Atom('y')), Atom('z'), merge=True)
>>> a3 = Atom('x') | Atom('y') | Atom('z')
>>>
>>> repr(a1)
"Or[Or[Atom('x'), Atom('y')], Atom('z')]"
>>> repr(a2)
"Or[Atom('x'), Atom('y'), Atom('z')]"
>>> repr(a2)
"Or[Atom('x'), Atom('y'), Atom('z')]"
>>>
>>> id(a1) == id(a2)
False
>>>
>>> id(a2) == id(a3)
True  # formulas a2 and a3 refer to the same object

Note

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformulas and creates a new formula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = x | y | z
>>>
>>> print(a.simplified(assumptions=[y]))
T  # True
>>> print(a.simplified(assumptions=[~y]))
x | z

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

Additionally, WCNFPlus support pseudo-Boolean constraints, i.e. weighted linear constraints by extending the above format. Basically, a pseudo-Boolean constraint needs to specify all the summands as weight*literal with the entire constraint being prepended with character w as follows:

c Example: One cardinality constraint and one PB constraint followed by a soft clause
p wcnf+ 7 3 10
10 1 -2 3 5 -7 <= 3
10 w 1*4 2*5 1*6 3*-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]]

class pysat.formula.XOr(*args, **kwargs)#

Exclusive disjunction. Given a list of operands (subformulas) \(f_i\), \(i \in \{1,\ldots,n\}, n \in \mathbb{N}\), it creates a formula \(f_1 \oplus f_2 \oplus\ldots\oplus f_n\). The list of operands of size at least 2 should be passed as arguments to the constructor.

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> xor = XOr(x, y, z)

If an additional Boolean keyword argument merge is provided set to True, the toolkit will try to flatten the current XOr formula merging its equivalence sub-operands into the list of operands. For example, if XOr(XOr(x, y), z, merge=True) is called, a new Formula object will be created with two operands: XOr(x, y) and z, followed by merging x and y into the list of root-level XOr. This will result in a formula XOr(x, y, z). Merging sub-operands is disabled by default if bitwise operations are used to create XOr formulas.

Example:

>>> from pysat.formula import *
>>> a1 = XOr(XOr(Atom('x'), Atom('y')), Atom('z'))
>>> a2 = XOr(XOr(Atom('x'), Atom('y')), Atom('z'), merge=True)
>>> a3 = Atom('x') ^ Atom('y') ^ Atom('z')
>>>
>>> print(a1)
(x ^ y) ^ z
>>> print(a2)
x ^ y ^ z
>>> print(a3)
(x ^ y) ^ z
>>>
>>> id(a1) == id(a2)
False
>>>
>>> id(a1) == id(a3)
True  # formulas a1 and a3 refer to the same object

Note

simplified(assumptions=[])#

Given a list of assumption literals, recursively simplifies the subformulas and creates a new formula.

Parameters:: assumptions (list(Formula)) – atomic assumptions
Return type:: Formula

Example:

>>> from pysat.formula import *
>>> x, y, z = Atom('x'), Atom('y'), Atom('z')
>>> a = x ^ y ^ z
>>>
>>> print(a.simplified(assumptions=[y]))
~x ^ z
>>> print(a.simplified(assumptions=[~y]))
x ^ z

Cardinality encodings (pysat.card)

External engines (pysat.engines)

Boolean formula manipulation (pysat.formula)#

List of classes#

Module description#

Module details#

Boolean formula manipulation (`pysat.formula`)#