1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
#!/usr/bin/env python
# -*- coding: utf-8 -*-
# Copyright (C) 2022 Authors of CryptoMiniSat, see AUTHORS file
#
# This program is free software; you can redistribute it and/or
# modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; version 2
# of the License.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
# 02110-1301, USA.
# hard example
# ----------------
# ../scripts/create_random_bnn.py 300 3000 100 4 > test.bnn
# ./cryptominisat5 --occsimp 0 --scc 0 test.bnn --presimp 0 --varelim 0 --verb 1 -n1 --printsol 0
# very hard example
#-------------
# ../scripts/create_random_bnn.py 300 2000 100 7 > test.bnn
# ./cryptominisat5 --occsimp 0 --scc 0 test.bnn --presimp 0 --varelim 0 --verb 4 -n1 --printsol 0
# appmc counting this:
# c [appmc] [ 21.46 ] bounded_sol_count looking for 73 solutions -- hashes active: 128
# c [appmc] [ 39.18 ] bounded_sol_count looking for 73 solutions -- hashes active: 256
# c [appmc] [ 117.86 ] bounded_sol_count looking for 73 solutions -- hashes active: 512
# more constraints than above
# --------------
# ../scripts/create_random_bnn.py 400 2000 100 9 > test.bnn
#c [appmc+arjun] Total time: 214.48
#c [appmc] Number of solutions is: 33*2**257
#s SATISFIABLE
#s mc 7642277889662868897955685010573401918315818987932277226604200544522266556235776
# BUG in appmc: test.bnn-appmcbug (also, bug-appmc in approxmc/build directory)
# kinda interesting one to run
# ---------------
# ../scripts/create_random_bnn.py 20 100 50 9 > test.bnn
# c Total time (this thread) : 41.60
# c [appmc+arjun] Total time: 41.59
# c [appmc] Number of solutions is: 52*2**59
import random
import sys
n = 100 # number of constraints
v = 1000 # number of variables
s = 30 # max size of constraints
seed = 1
if len(sys.argv) != 1:
if len(sys.argv) != 5:
print("ERROR: must give: n v s seed")
exit(-1)
n = int(sys.argv[1])
v = int(sys.argv[2])
s = int(sys.argv[3])
seed = int(sys.argv[4])
assert n > 10
assert v > 0
random.seed(seed)
print("c n=%d v=%d seed=%d" % (n, v, seed))
for x in range(n):
sz = random.randint(1,s)
# get input + output
ks = []
while len(ks) < sz+1:
x = random.randint(1,v)
if x in ks or -x in ks:
continue
else:
ks.append(x)
# get cutoff
cutoff = random.randint(0, sz)
# get output
output = ks[len(ks)-1]
ks = ks[:-1]
pr = "b "
for k in ks:
if random.choice([True, False]):
pr+="-"
pr += "%d " % k
pr += "0 "
pr += "%d " % cutoff
pr += "%d" % output
print("%s" % pr)
# add some clauses
for x in range(n):
sz = random.randint(1,8)
ks = []
while len(ks) < sz:
x = random.randint(1, v)
if x in ks or -x in ks:
continue
if random.choice([True, False]):
ks.append(x)
else:
ks.append(-x)
pr = ""
for k in ks:
pr += "%d " % k
print("%s0" % pr)
|
