| | |
- __builtin__.object
-
- CNFEncoder
-
- CryptoMiniSatEncoder
class CNFEncoder(__builtin__.object) |
| | |
Methods defined here:
- __init__(self, r, random_seed=16)
- clauses(self, f)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
[{...x: 0...}]
>>> e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
[{...x: 1...}, {...y: 1...}]
>>> [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
[[(z, 0), (y, 0), (x, 0)]]
>>> [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
[[(y, 1), (x, 0)], [(y, 0), (x, 1)]]
- dimacs_cnf(self, polynomial_system)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0'
>>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 2\n1 -2 0\n-1 2 0'
>>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 3\n-1 -2 -3 0\n-1 2 0\n1 -2 0'
- dimacs_encode_clause(self, c)
- dimacs_encode_polynomial(self, p)
- >>> from polybori import *
>>> d=dict()
>>> r = declare_ring(["x", "y", "z"], d)
>>> e = CNFEncoder(r)
>>> e.dimacs_encode_polynomial(d["x"]+d["y"]+d["z"])
['1 2 -3 0', '1 -2 3 0', '-1 -2 -3 0', '-1 2 3 0']
- polynomial_clauses(self, f)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
[x*y*z]
>>> v = r.variable
>>> p = v(1)*v(2)+v(2)*v(0)+1
>>> groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
True
- to_dimacs_index(self, v)
- zero_blocks(self, f)
- divides the zero set of f into blocks
>>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
[{y: 0}, {z: 0}, {x: 0}]
Data descriptors defined here:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
|
class CryptoMiniSatEncoder(CNFEncoder) |
| | |
- Method resolution order:
- CryptoMiniSatEncoder
- CNFEncoder
- __builtin__.object
Methods defined here:
- dimacs_cnf(self, polynomial_system)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CryptoMiniSatEncoder(r)
>>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2)])
'c cnf generated by PolyBoRi\np cnf 3 1\n-1 -2 -3 0\nc g 1 x*y*z\nc v 1 x\nc v 2 y\nc v 3 z'
>>> e.dimacs_cnf([r.variable(1)+r.variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 1\nx1 2 0\nc g 2 x + y\nc v 1 x\nc v 2 y'
>>> e.dimacs_cnf([r.variable(0)*r.variable(1)*r.variable(2), r.variable(1)+r.variable(0)])
'c cnf generated by PolyBoRi\np cnf 3 2\n-1 -2 -3 0\nc g 3 x*y*z\nx1 2 0\nc g 4 x + y\nc v 1 x\nc v 2 y\nc v 3 z'
- dimacs_encode_polynomial(self, p)
- >>> from polybori import *
>>> d=dict()
>>> r = declare_ring(["x", "y", "z"], d)
>>> e = CryptoMiniSatEncoder(r)
>>> p = d["x"]+d["y"]+d["z"]
>>> p.deg()
1
>>> len(p)
3
>>> e.dimacs_encode_polynomial(p)
['x1 2 3 0\nc g 1 x + y + z']
>>> e.dimacs_encode_polynomial(p+1)
['x1 2 -3 0\nc g 2 x + y + z + 1']
Data and other attributes defined here:
- group_counter = 0
Methods inherited from CNFEncoder:
- __init__(self, r, random_seed=16)
- clauses(self, f)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.clauses(r.variable(0)*r.variable(1)*r.variable(2)) # doctest:+ELLIPSIS
[{...x: 0...}]
>>> e.clauses(r.variable(1)+r.variable(0)) # doctest:+ELLIPSIS
[{...x: 1...}, {...y: 1...}]
>>> [sorted(c.iteritems()) for c in e.clauses(r.variable(0)*r.variable(1)*r.variable(2))]
[[(z, 0), (y, 0), (x, 0)]]
>>> [sorted(c.iteritems()) for c in e.clauses(r.variable(1)+r.variable(0))]
[[(y, 1), (x, 0)], [(y, 0), (x, 1)]]
- dimacs_encode_clause(self, c)
- polynomial_clauses(self, f)
- >>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.polynomial_clauses(r.variable(0)*r.variable(1)*r.variable(2))
[x*y*z]
>>> v = r.variable
>>> p = v(1)*v(2)+v(2)*v(0)+1
>>> groebner_basis([p], heuristic = False)==groebner_basis(e.polynomial_clauses(p), heuristic = False)
True
- to_dimacs_index(self, v)
- zero_blocks(self, f)
- divides the zero set of f into blocks
>>> from polybori import *
>>> r = declare_ring(["x", "y", "z"], dict())
>>> e = CNFEncoder(r)
>>> e.zero_blocks(r.variable(0)*r.variable(1)*r.variable(2))
[{y: 0}, {z: 0}, {x: 0}]
Data descriptors inherited from CNFEncoder:
- __dict__
- dictionary for instance variables (if defined)
- __weakref__
- list of weak references to the object (if defined)
| |