File: bnn_create_random.py

package info (click to toggle)
cryptominisat 5.11.4%2Bdfsg1-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 4,432 kB
  • sloc: cpp: 55,148; ansic: 9,642; python: 8,899; sh: 1,336; php: 477; sql: 403; javascript: 173; xml: 34; makefile: 15
file content (129 lines) | stat: -rwxr-xr-x 3,439 bytes parent folder | download | duplicates (2)
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)