Details of instance load_3c_comp_comp7_REAL.aag

Name: load_3c_comp_comp7_REAL.aag
md5: 96f00e2d0e63cae7b9e4736f3a400fcb
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 (130.2 kB)
aag 8353 7 666 1 7680
2
4
6
8
10
12
14
16 0
18 4251
20 4255
22 4259
24 4263
26 4267
28 4271
30 4275
32 4283
34 0
36 3945
38 3949
40 3953
42 3957
44 3961
46 3965
48 3969
50 3977
52 0
54 3763
56 3767
58 3771
60 3775
62 3779
64 3783
66 3787
68 3795
70 4231
72 4233
74 4235
76 4237
78 4239
80 4241
82 4243
84 4245
86 4247
88 3799
90 3803
92 3807
94 3811
96 3815
98 3819
100 3823
102 3827
104 3831
106 0
108 3403
110 3407
112 3411
114 3415
116 3419
118 3423
120 3427
122 3435
124 0
126 3367
128 3371
130 3375
132 3379

... [truncated 129.2 kB]


l639 latch639
l640 latch640
l641 latch641
l642 latch642
l643 latch643
l644 latch644
l645 latch645
l646 latch646
l647 latch647
l648 latch648
l649 latch649
l650 latch650
l651 latch651
l652 latch652
l653 latch653
l654 latch654
l655 latch655
l656 latch656
l657 latch657
l658 latch658
l659 latch659
l660 latch660
l661 latch661
l662 latch662
l663 latch663
l664 latch664
l665 latch665
o0 error
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 2/3 [2015-pre-classification]
SOLVED_IN : 41.8743 [2015-pre-classification]
#.