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)
|