brickenstein / polybori-scripts
Scripts for PolyBoRi
Clone this repository (size: 15.9 KB): HTTPS / SSH
$ hg clone http://bitbucket.org/brickenstein/polybori-scripts/
| commit 12: | 4f1a2994dd6f |
| parent 11: | 22b23baa2d80 |
| branch: | default |
initial support for variable/clause groups/have to test it
Changed (Δ1.3 KB):
raw changeset »
cnf.py (27 lines added, 5 lines removed)
| … | … | @@ -2,6 +2,7 @@ from random import Random |
2 |
2 |
from polybori.PyPolyBoRi import Monomial, Variable, BooleSet, Polynomial, if_then_else as ite,\ |
3 |
3 |
change_ordering, lp, gauss_on_polys, global_ring, ll_red_nf_redsb |
4 |
4 |
from polybori.ll import ll_encode |
5 |
from polybori.statistics import used_vars_set |
|
5 |
6 |
class CNFEncoder(object): |
6 |
7 |
def __init__(self, r, random_seed = 16): |
7 |
8 |
self.random_generator = Random(random_seed) |
| … | … | @@ -150,8 +151,9 @@ class CNFEncoder(object): |
150 |
151 |
res.append(c) |
151 |
152 |
return "\n".join(res) |
152 |
153 |
class CryptoMiniSatEncoder(CNFEncoder): |
154 |
group_counter=0 |
|
153 |
155 |
def dimacs_encode_polynomial(self, p): |
154 |
|
|
156 |
r""" |
|
155 |
157 |
>>> from polybori import * |
156 |
158 |
>>> d=dict() |
157 |
159 |
>>> r = declare_ring(["x", "y", "z"], d) |
| … | … | @@ -162,13 +164,14 @@ class CryptoMiniSatEncoder(CNFEncoder): |
162 |
164 |
>>> len(p) |
163 |
165 |
3 |
164 |
166 |
>>> e.dimacs_encode_polynomial(p) |
165 |
['x1 2 3 |
|
167 |
['x1 2 3\nc g 1 x + y + z'] |
|
166 |
168 |
>>> e.dimacs_encode_polynomial(p+1) |
167 |
['x1 2 -3 |
|
169 |
['x1 2 -3\nc g 2 x + y + z + 1'] |
|
168 |
170 |
""" |
169 |
171 |
if p.deg()!=1 or len(p)<=1: |
170 |
re |
|
172 |
res = super(CryptoMiniSatEncoder, self).dimacs_encode_polynomial(p) |
|
171 |
173 |
else: |
174 |
||
172 |
175 |
if p.has_constant_part(): |
173 |
176 |
invert_last = True |
174 |
177 |
else: |
| … | … | @@ -177,7 +180,26 @@ class CryptoMiniSatEncoder(CNFEncoder): |
177 |
180 |
indices = [self.to_dimacs_index(v) for v in variables] |
178 |
181 |
if invert_last: |
179 |
182 |
indices[-1]=-indices[-1] |
180 |
re |
|
183 |
res = ["x"+" ".join([str(v) for v in indices])] |
|
184 |
self.group_counter = self.group_counter + 1 |
|
185 |
group_comment="\nc g %s %s" %(self.group_counter, str(p)[:30]) |
|
186 |
return [c+group_comment for c in res] |
|
187 |
def dimacs_cnf(self, polynomial_system): |
|
188 |
r""" |
|
189 |
>>> from polybori import * |
|
190 |
>>> r = declare_ring(["x", "y", "z"], dict()) |
|
191 |
>>> e = CryptoMiniSatEncoder(r) |
|
192 |
>>> e.dimacs_cnf([Variable(0)*Variable(1)*Variable(2)]) |
|
193 |
'c cnf generated by PolyBoRi\np cnf 3 1\n-2 -3 -1 0\nc g 1 x*y*z\nc v 1 x\nc v 2 y\nc v 3 z' |
|
194 |
>>> e.dimacs_cnf([Variable(1)+Variable(0)]) |
|
195 |
'c cnf generated by PolyBoRi\np cnf 3 1\nx1 2\nc g 2 x + y\nc v 1 x\nc v 2 y' |
|
196 |
>>> e.dimacs_cnf([Variable(0)*Variable(1)*Variable(2), Variable(1)+Variable(0)]) |
|
197 |
'c cnf generated by PolyBoRi\np cnf 3 2\n-2 -3 -1 0\nc g 3 x*y*z\nx1 2\nc g 4 x + y\nc v 1 x\nc v 2 y\nc v 3 z' |
|
198 |
""" |
|
199 |
uv=list(used_vars_set(polynomial_system).variables()) |
|
200 |
res=super(CryptoMiniSatEncoder, self).dimacs_cnf(polynomial_system) |
|
201 |
res=res+"\n"+"\n".join(["c v %s %s"% (self.to_dimacs_index(v), v) for v in uv]) |
|
202 |
return res |
|
181 |
203 |
def _test(): |
182 |
204 |
import doctest |
183 |
205 |
doctest.testmod() |