Secure your code as it's written. Use Snyk Code to scan source code in minutes - no build needed - and fix issues immediately.
>>> print(cnf.clauses)
[[-3, 4], [5, 6], [3], [-4], [-5], [-6]]
"""
cnf = CNF()
cnf.nv = self.nv
cnf.clauses = copy.deepcopy(self.hard) + copy.deepcopy(self.soft)
cnf.commends = self.comments[:]
return cnf
#
#==============================================================================
class CNFPlus(CNF, object):
"""
CNF formulas augmented with *native* cardinality constraints.
This class inherits most of the functionality of the :class:`CNF`
class. The only difference between the two is that :class:`CNFPlus`
supports *native* cardinality constraints of `MiniCard
`__.
The parser of input DIMACS files of :class:`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
Example:
.. code-block:: python
>>> 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]]
"""
cnf = CNF()
cnf.nv = self.nv
cnf.clauses = copy.deepcopy(self.hard) + copy.deepcopy(self.soft)
cnf.commends = self.comments[:]
return 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
.. code-block:: python
>>> 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, -3]
"""
negated = CNF()
negated.nv = topv
if not negated.nv:
negated.nv = self.nv
negated.clauses = []
negated.auxvars = []
for cl in self.clauses:
auxv = -cl[0]
if len(cl) > 1:
negated.nv += 1
auxv = negated.nv
# direct implication
for l in cl:
# pseudo-Boolean constraint and variable manager
constr = pblib.PBConstraint(wlits, EncType._to_pbcmp[comparator], bound)
varmgr = pblib.AuxVarManager(top_id + 1)
# encoder configuration
config = pblib.PBConfig()
config.set_PB_Encoder(EncType._to_pbenc[encoding])
# encoding
result = pblib.VectorClauseDatabase(config)
pb2cnf = pblib.Pb2cnf(config)
pb2cnf.encode(constr, result, varmgr)
# extracting clauses
ret = CNF(from_clauses=result.get_clauses())
# updating vpool if necessary
if vpool:
if vpool._occupied and vpool.top <= vpool._occupied[0][0] <= ret.nv:
cls._update_vids(ret, vpool)
else:
vpool.top = ret.nv - 1
vpool._next()
return ret
for comb in itertools.combinations(pigeons, kval + 1):
self.append([-var(i, j) for i in comb])
if verb:
head = 'c {0}PHP formula for'.format('' if kval == 1 else str(kval) + '-')
head += ' {0} pigeons and {1} holes'.format(kval * nof_holes + 1, nof_holes)
self.comments.append(head)
for i in range(1, kval * nof_holes + 2):
for j in range(1, nof_holes + 1):
self.comments.append('c (pigeon, hole) pair: ({0}, {1}); bool var: {2}'.format(i, j, var(i, j)))
#
#==============================================================================
class GT(CNF, object):
"""
Generator of ordering (or *greater than*, GT) principle formulas. Given
an integer parameter :math:`n`, the principle states that any partial
order on the set :math:`\{1,2,\ldots,n\}` must have a maximal element.
Assume variable :math:`x_{ij}`, for :math:`i,j\in[n],i\\neq j`, denotes
the fact that :math:`i \succ j`. Clauses :math:`(\\neg{x_{ij}} \\vee
\\neg{x_{ji}})` and :math:`(\\neg{x_{ij}} \\vee \\neg{x_{jk}} \\vee
x_{ik})` ensure that the relation :math:`\succ` is anti-symmetric and
transitive. As a result, :math:`\succ` is a partial order on
:math:`[n]`. The additional requirement that each element :math:`i` has
a successor in :math:`[n]\setminus\{i\}` represented a clause
:math:`(\\vee_{j \\neq i}{x_{ji}})` makes the formula unsatisfiable.
GT formulas were originally conjectured [2]_ to be hard for resolution.
However, [5]_ proved the existence of a polynomial size resolution
print(' Available values: [0 .. FLOAT_MAX], none (default: none)')
print(' -v, --verbose Be verbose')
#
#==============================================================================
if __name__ == '__main__':
print_model, solver, timeout, verbose, files = parse_options()
if files:
# reading standard CNF or WCNF
if re.search('cnf(\.(gz|bz2|lzma|xz))?$', files[0]):
if re.search('\.wcnf(\.(gz|bz2|lzma|xz))?$', files[0]):
formula = WCNF(from_file=files[0])
else: # expecting '*.cnf'
formula = CNF(from_file=files[0]).weighted()
lsu = LSU(formula, solver=solver,
expect_interrupt=(timeout != None), verbose=verbose)
# reading WCNF+
elif re.search('\.wcnf[p,+](\.(gz|bz2|lzma|xz))?$', files[0]):
formula = WCNFPlus(from_file=files[0])
lsu = LSUPlus(formula, expect_interrupt=(timeout != None),
verbose=verbose)
# setting a timer if necessary
if timeout is not None:
if verbose > 1:
print('c timeout: {0}'.format(timeout))
timer = Timer(timeout, lambda s: s.interrupt(), [lsu])
#
#==============================================================================
from __future__ import print_function
import collections
import getopt
import itertools
import os
from pysat.card import *
from pysat.formula import IDPool, CNF
from six.moves import range
import sys
#
#==============================================================================
class PHP(CNF, object):
"""
Generator of :math:`k` pigeonhole principle (:math:`k`-PHP) formulas.
Given integer parameters :math:`m` and :math:`k`, the :math:`k`
pigeonhole principle states that if :math:`k\cdot m+1` pigeons are
distributes by :math:`m` holes, then at least one hole contains more
than :math:`k` pigeons.
Note that if :math:`k` is 1, the principle degenerates to the
formulation of the original pigeonhole principle stating that
:math:`m+1` pigeons cannot be distributed by :math:`m` holes.
Assume that a Boolean variable :math:`x_{ij}` encodes that pigeon
:math:`i` resides in hole :math:`j`. Then a PHP formula can be seen as
a conjunction: :math:`\\bigwedge_{i=1}^{k\cdot
m+1}{\\textsf{AtLeast1}(x_{i1},\ldots,x_{im})}\wedge
\\bigwedge_{j=1}^{m}{\\textsf{AtMost}k(x_{1j},\ldots,x_{k\cdot
"""
if self.tobj:
if not self._merged:
pycard.itot_del(self.tobj)
# otherwise, this totalizer object is merged into a larger one
# therefore, this memory should be freed in its destructor
self.tobj = None
self.lits = []
self.ubound = 0
self.top_id = 0
self.cnf = CNF()
self.rhs = []
self.nof_new = 0
:return: an object of class :class:`CNF`.
Example:
.. code-block:: python
>>> cnf1 = CNF(from_clauses=[[-1, 2], [1]])
>>> cnf2 = cnf1.copy()
>>> print(cnf2.clauses)
[[-1, 2], [1]]
>>> print(cnf2.nv)
2
"""
cnf = CNF()
cnf.nv = self.nv
cnf.clauses = copy.deepcopy(self.clauses)
cnf.comments = copy.deepcopy(self.comments)
return cnf
self.extend(am1.clauses)
else: # atleast1 constrant for black cells
self.append(adj)
if verb:
head = 'c CB formula for the chessboard of size {0}x{0}'.format(2 * size)
head += '\nc The encoding is {0}exhaustive'.format('' if exhaustive else 'not ')
self.comments.append(head)
for v in range(1, vpool.top + 1):
self.comments.append('c {0}; bool var: {1}'.format(vpool.obj(v), v))
#
#==============================================================================
class PAR(CNF, object):
"""
Generator of the parity principle (PAR) formulas. Given an integer
parameter :math:`n`, the principle states that no graph on :math:`2n+1`
nodes consists of a complete perfect matching.
The encoding of the parity principle uses :math:`\\binom{2n+1}{2}`
variables :math:`x_{ij},i \\neq j`. If variable :math:`x_{ij}` is
*true*, then there is an edge between nodes :math:`i` and :math:`j`.
The formula consists of the following clauses: :math:`(\\vee_{j \\neq
i}{x_{ij}})` for every :math:`i\in[2n+1]`, and :math:`(\\neg{x_{ij}}
\\vee \\neg{x_{kj}})` for all distinct :math:`i,j,k \in [2n+1]`.
The parity principle is known to be hard for resolution [4]_.
:param size: problem size (:math:`n`)
:param topv: current top variable identifier