Boolean formula manipulation (pysat.formula
)#
List of classes#
A simple manager of variable IDs. |
|
Class for manipulating CNF formulas. |
|
CNF formulas augmented with native cardinality constraints. |
|
Class for manipulating partial (weighted) CNF formulas. |
|
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 characterc
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 withcomment_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 anaiger.BoolExpr
, or an*.aag
filename, or an AIGER string to parse. (Classesaiger.AIG
andaiger.BoolExpr
are defined in the py-aiger package.)- Parameters
aig (
aiger.AIG
(see py-aiger package)) – an input AIGER circuitvpool (
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 beNone
(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 thebackports.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 theenclits
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 beNone
(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 thebackports.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 to1
. 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 thatCNFPlus
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)
, wherelits
is a list of literals in the sum andk
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 toFalse
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, methodappend()
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 to1
. 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 thetop
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
tostop
(inclusive).- Parameters
start (int) – beginning of the interval.
stop (int) – end of the interval.
- 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 characterc
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
Note that the
compressed_with
parameter can beNone
(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 thebackports.lzma
package to be additionally installed.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
Note that the
compress_with
parameter can beNone
(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 thebackports.lzma
package to be additionally installed.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 theclauses
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 thatWCNFPlus
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 forCNFPlus
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)
, wherelits
is a list of literals in the sum andk
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 toFalse
by default.If
is_atmost
is set toFalse
, the clause can be either hard or soft depending on theweight
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
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 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 theclauses
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]]