Details of instance load_3c_comp_comp2_REAL.aag

Name: load_3c_comp_comp2_REAL.aag
md5: 7d95e96d2e89348043702dd4bea495f9
FractionOfBinaryClauses None
FractionOfNegativeLiteralsPerClauseEntropy None
FractionOfNegativeLiteralsPerClauseMax None
FractionOfNegativeLiteralsPerClauseMean None
FractionOfNegativeLiteralsPerClauseMin None
FractionOfNegativeLiteralsPerClauseVariationCoefficient None
FractionOfNegativeVariablesEntropy None
FractionOfNegativeVariablesMax None
FractionOfNegativeVariablesMean None
FractionOfNegativeVariablesMin None
FractionOfNegativeVariablesVariationCoefficient None
FractionOfPositiveLiteralsPerClauseEntropy None
FractionOfPositiveLiteralsPerClauseMax None
FractionOfPositiveLiteralsPerClauseMean None
FractionOfPositiveLiteralsPerClauseMin None
FractionOfPositiveLiteralsPerClauseVariationCoefficient None
FractionOfPositiveVariablesEntropy None
FractionOfPositiveVariablesMax None
FractionOfPositiveVariablesMean None
FractionOfPositiveVariablesMin None
FractionOfPositiveVariablesVariationCoefficient None
FractionOfTernaryClauses None
FractionOfUnaryClauses None
ClausesToVariablesRatio None
ClausesToVariablesRatioCubic None
ClausesToVariablesRatioQuadratic None
LinearizedClausesToVariablesRatio None
LinearizedClausesToVariablesRatioQuadratic None
LinearizedClaustesToVariablesRatioCubic None
NumberOfClauses None
NumberOfVariables None
VariablesToClausesRatio None
VariablesToClausesRatioCubic None
VariablesToClausesRatioQuadratic None
ClauseNodeDegreesEntropy None
ClauseNodeDegreesMax None
ClauseNodeDegreesMean None
ClauseNodeDegreesMin None
ClauseNodeDegreesVariationCoefficient None
VariableNodeDegreesEntropy None
VariableNodeDegreesMax None
VariableNodeDegreesMean None
VariableNodeDegreesMin None
VariableNodeDegreesVariationCoefficient None
DegreeEntropy None
DegreeMax None
DegreeMean None
DegreeMin None
DegreeVariationCoefficient None
Download instance (55.0 kB)
aag 3883 7 296 1 3580
2
4
6
8
10
12
14
16 0
18 1961
20 1965
22 1973
24 0
26 1825
28 1829
30 1837
32 0
34 1743
36 1747
38 1755
40 1951
42 1953
44 1955
46 1957
48 1759
50 1763
52 1767
54 1771
56 0
58 1583
60 1587
62 1595
64 0
66 1567
68 1571
70 1579
72 1337
74 1341
76 1345
78 1349
80 0
82 1977
84 1981
86 1989
88 1321
90 1325
92 1329
94 1333
96 1793
98 1797
100 1801
102 1805
104 1775
106 1779
108 1783
110 1787
112 1937
114 1941
116 1945
118 1949
120 1993
122 1997
124 2001
126 2005
128 1809
130 1813
132 1817
13

... [truncated 54.0 kB]


l269 latch269
l270 latch270
l271 latch271
l272 latch272
l273 latch273
l274 latch274
l275 latch275
l276 latch276
l277 latch277
l278 latch278
l279 latch279
l280 latch280
l281 latch281
l282 latch282
l283 latch283
l284 latch284
l285 latch285
l286 latch286
l287 latch287
l288 latch288
l289 latch289
l290 latch290
l291 latch291
l292 latch292
l293 latch293
l294 latch294
l295 latch295
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 2.15502 [2015-pre-classification]
#.