Skip to content

Commit 73413bc

Browse files
ebhardjanebhardjan
committed
adding 2 unsat and 2 more sat formulas
1 parent 70b0810 commit 73413bc

File tree

6 files changed

+1056
-3
lines changed

6 files changed

+1056
-3
lines changed

‎cnfs/benchmark_formulas/README.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,15 @@
11
# Benchmark CNFs
22

3-
There are 12 formulas in our benchmark set and we tried to pick them from
4-
different real world problems.
3+
There are 14 formulas in our benchmark set and we tried to pick them from
4+
different real world problems as well as some random ones.
55

66

77
| Files | Description | Reference |
88
| ----- | ----------- | --------- |
9-
| 2bitcomp_5.cnf, 2bitmax_5.cnf | Circuit Verification Problems from SAT Challenge Beijing 1996 | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/Bejing/bejing.descr.html)
109
| anomaly.cnf, medium.cnf | SAT-encoded Blocks World Planning Problems | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/PLANNING/BlocksWorld/descr.html)
1110
| ais6.cnf, ais8.cnf | SAT-encoded All-Interval Series Problems | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/AIS/descr.html)
1211
| flat(50/75)-x.cnf | SAT-encoded "Flat" Graph coloring problems (J. Coberson's flat graph generator is used) | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/GCP/descr.html)
1312
| ii8a(1/2).cnf | Inductive Inference, stem from a formulation of Boolean Function Synthesis Problems | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/II/descr.html)
1413
| par8-1-c.cnf, par8-5.cnf | Instances for Learning the Paritiy Function | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/PARITY/descr.html)
14+
| uf50/75-01.cnf | Uniform Random 3-sat, sat | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html)
15+
| uuf50-01/02.cnf | Uniform Random 3-sat, unsat | [www.cs.ubc.ca](http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html)

‎cnfs/benchmark_formulas/uf50-01.cnf

Lines changed: 226 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,226 @@
1+
c This Formular is generated by mcnf
2+
c
3+
c horn? no
4+
c forced? no
5+
c mixed sat? no
6+
c clause length = 3
7+
c
8+
p cnf 50 218
9+
-3 36 7 0
10+
-3 -42 -48 0
11+
-49 -47 -41 0
12+
8 -40 17 0
13+
-21 -31 -39 0
14+
36 -22 49 0
15+
27 38 14 0
16+
15 -18 6 0
17+
6 7 -43 0
18+
34 -7 23 0
19+
2 14 -13 0
20+
2 47 -42 0
21+
-33 -35 3 0
22+
44 40 49 0
23+
50 36 31 0
24+
-36 -3 -37 0
25+
26 -29 43 0
26+
15 29 -45 0
27+
24 -11 18 0
28+
-47 -26 6 0
29+
-50 -33 -10 0
30+
32 6 16 0
31+
-34 37 41 0
32+
7 -28 -17 0
33+
-44 46 19 0
34+
7 22 -48 0
35+
3 39 34 0
36+
31 46 -43 0
37+
-27 32 23 0
38+
37 -50 -18 0
39+
20 5 11 0
40+
-45 -24 6 0
41+
-34 -23 -14 0
42+
-22 21 20 0
43+
-17 50 24 0
44+
-25 -24 -27 0
45+
3 35 21 0
46+
-26 47 -36 0
47+
-28 -45 49 0
48+
-21 -6 12 0
49+
-17 -15 -39 0
50+
41 2 -14 0
51+
25 36 -23 0
52+
-39 -3 -40 0
53+
50 20 35 0
54+
27 31 -39 0
55+
45 -15 -40 0
56+
34 50 35 0
57+
-1 -48 12 0
58+
18 -35 -30 0
59+
27 -24 -25 0
60+
-4 -33 -12 0
61+
-43 -24 -37 0
62+
-37 31 -44 0
63+
-9 -38 14 0
64+
33 -16 34 0
65+
4 -35 -5 0
66+
-3 -21 -19 0
67+
-35 -36 -29 0
68+
7 -43 36 0
69+
30 14 41 0
70+
-35 -24 -7 0
71+
35 -42 6 0
72+
-1 -15 39 0
73+
27 49 -16 0
74+
-37 49 -10 0
75+
50 -46 -3 0
76+
-41 20 34 0
77+
-1 23 28 0
78+
-12 -30 -20 0
79+
-24 29 -37 0
80+
12 5 -44 0
81+
-6 -2 48 0
82+
-2 -49 -43 0
83+
1 -50 24 0
84+
-7 -50 -44 0
85+
-41 43 4 0
86+
13 15 -11 0
87+
-3 -11 23 0
88+
33 48 41 0
89+
9 23 -49 0
90+
-43 47 1 0
91+
-40 16 -29 0
92+
30 19 3 0
93+
19 -34 48 0
94+
-16 -44 14 0
95+
38 -45 -12 0
96+
-4 -14 -31 0
97+
-48 35 -1 0
98+
45 -13 19 0
99+
9 42 -7 0
100+
-1 -15 8 0
101+
-13 -44 -14 0
102+
-43 -37 -31 0
103+
-27 -29 47 0
104+
7 4 17 0
105+
7 10 35 0
106+
-25 20 17 0
107+
35 -5 -42 0
108+
-50 24 -5 0
109+
-21 -26 2 0
110+
-8 45 -21 0
111+
-16 33 49 0
112+
-38 6 16 0
113+
5 21 37 0
114+
8 38 31 0
115+
-21 33 14 0
116+
20 40 -5 0
117+
-29 -9 31 0
118+
-7 42 -22 0
119+
-48 8 26 0
120+
48 -38 33 0
121+
-34 49 46 0
122+
-14 -46 25 0
123+
-46 4 18 0
124+
36 -12 -31 0
125+
12 -18 14 0
126+
-7 46 -16 0
127+
9 -8 7 0
128+
49 -42 -22 0
129+
22 -15 38 0
130+
34 -41 47 0
131+
22 -26 32 0
132+
-25 -45 -21 0
133+
-26 32 -11 0
134+
15 26 -25 0
135+
-1 46 25 0
136+
-14 -31 30 0
137+
-9 -22 12 0
138+
-18 26 -35 0
139+
-16 -32 -21 0
140+
31 -49 -21 0
141+
11 9 41 0
142+
-13 -30 19 0
143+
-10 4 6 0
144+
-4 3 -22 0
145+
-25 -50 -18 0
146+
-40 4 9 0
147+
37 20 46 0
148+
-27 22 -29 0
149+
34 14 3 0
150+
3 -31 20 0
151+
-50 2 -26 0
152+
17 -29 38 0
153+
-49 12 -41 0
154+
15 -35 -43 0
155+
-22 -23 -49 0
156+
-9 33 48 0
157+
26 29 35 0
158+
27 -50 37 0
159+
-7 46 -43 0
160+
-46 -37 -8 0
161+
-40 36 -24 0
162+
-44 46 15 0
163+
-3 36 -16 0
164+
-48 9 43 0
165+
-25 -4 44 0
166+
-22 37 -7 0
167+
-31 -17 -22 0
168+
-11 -48 17 0
169+
23 34 -28 0
170+
23 -48 -39 0
171+
-37 -1 -23 0
172+
-19 27 14 0
173+
-22 33 -6 0
174+
-6 -32 -26 0
175+
18 -20 -46 0
176+
43 22 27 0
177+
-13 34 49 0
178+
-35 -46 3 0
179+
32 39 -43 0
180+
6 -39 -9 0
181+
27 39 -16 0
182+
25 -17 -15 0
183+
-43 27 34 0
184+
-6 49 5 0
185+
-38 11 14 0
186+
40 -38 47 0
187+
37 -14 17 0
188+
39 29 36 0
189+
-39 -28 1 0
190+
-18 14 -16 0
191+
-40 50 15 0
192+
37 -42 18 0
193+
-13 31 33 0
194+
2 -42 33 0
195+
8 -3 -22 0
196+
1 23 -31 0
197+
-20 -45 26 0
198+
42 11 49 0
199+
29 11 -43 0
200+
-20 -21 30 0
201+
23 45 -35 0
202+
38 -30 -14 0
203+
-9 48 -29 0
204+
11 -18 -23 0
205+
-41 -1 -29 0
206+
5 41 26 0
207+
44 -30 -7 0
208+
38 -6 -41 0
209+
46 48 -15 0
210+
-18 -10 -47 0
211+
38 46 -32 0
212+
-32 46 12 0
213+
31 40 14 0
214+
-18 2 49 0
215+
28 -38 27 0
216+
-16 -21 14 0
217+
-29 15 12 0
218+
49 34 5 0
219+
14 22 -12 0
220+
30 33 20 0
221+
-24 22 25 0
222+
4 -48 -23 0
223+
-30 -36 9 0
224+
44 12 -35 0
225+
38 3 -21 0
226+
-11 33 49 0

0 commit comments

Comments
 (0)