Details of instance load_4c_comp_comp3_REAL.aag

Name: load_4c_comp_comp3_REAL.aag
md5: 20ecedb710ab3c51e7f5bcd9ae9c8ce8
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 (95.5 kB)
aag 6381 9 480 1 5892
2
4
6
8
10
12
14
16
18
20 0
22 2677
24 2681
26 2685
28 2693
30 0
32 2507
34 2511
36 2515
38 2523
40 0
42 2403
44 2407
46 2411
48 2419
50 2665
52 2667
54 2669
56 2671
58 2673
60 2423
62 2427
64 2431
66 2435
68 2439
70 0
72 2203
74 2207
76 2211
78 2219
80 0
82 2183
84 2187
86 2191
88 2199
90 1895
92 1899
94 1903
96 1907
98 1911
100 0
102 2697
104 2701
106 2705
108 2713
110 1875
112 1879
114 1883
116 1887
118 1891
120 2467
122 2471
124 2475
126 2479
128 2483
130 2443
132 2447
134 2451
136

... [truncated 94.5 kB]


l453 latch453
l454 latch454
l455 latch455
l456 latch456
l457 latch457
l458 latch458
l459 latch459
l460 latch460
l461 latch461
l462 latch462
l463 latch463
l464 latch464
l465 latch465
l466 latch466
l467 latch467
l468 latch468
l469 latch469
l470 latch470
l471 latch471
l472 latch472
l473 latch473
l474 latch474
l475 latch475
l476 latch476
l477 latch477
l478 latch478
l479 latch479
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 111.043 [2015-pre-classification]
#.