PBSugar: Experimental Results

Table of Contents

Overview

This web page reports the experimental results of PBSugar version 1.1 for all 669 instances of DEC-SMALLINT-LIN (decision problems, small integers, linear constraints) category of 2011 PB competition benchmark set. The following solvers are executed on our environment.

NameDescriptionReference
PBSugarPBSugar version 1.1
Sat4jSat4j PB Res//CP version 2.3.2Le Berre and Parrain {BerreP10}
claspclasp version 2.1.1 (64-bit code)Gebser et al. {GebserKNS07}
bsolobsolo version 3.2 (32-bit code)Manquinho and Silva {ManquinhoS06}
wbowbo version 1.4a (32-bit code)Manquinho et al. {ManquinhoML10}
MiniSat+MiniSat+ version 1.0 (64-bit code)Eén and Sörensson {EenS06}
  • Sat4j PB Rees//CP version 2.3.2 was ranked first in 2012 PB competition DEC-SMALLINT-LIN category.
  • clasp version 2.1.1 is a newer version of clasp version 2.0.6 which was ranked second as the submitted solver in 2012 PB competition DEC-SMALLINT-LIN category.
  • bsolo version 3.2 was ranked third in 2010 PB competition DEC-SMALLINT-LIN category, and its 32-bit binary code is avaiable from 2010 PB competition site.
  • wbo version 1.4a was ranked fourth in 2010 PB competition DEC-SMALLINT-LIN category, and its 32-bit binary code is avaiable from 2010 PB competition site.
  • MiniSat+ version 1.0 was ranked third in 2006 PB competition SATUNSAT-SMALLINT category, and its source code is avaiable from MiniSat+ site.
  • See http://www.cril.univ-artois.fr/PB12/results/ranking.php?idev=67 for the ranking in 2012 PB competition DEC-SMALLINT-LIN category.

Machine Specification and Software Versions

  • CPU: Intel Dual Core Xeon X5260 (L2 cache 6MB) 3.33GHz x 2 (6650 bogomips)
  • Memory: 16GB (4 x 4GB DDR2 SDRAM)
  • OS: Linux kernel version 3.2.0 generic x86_64 (Ubuntu Linux 12.04)
  • Java: Java version 1.6.0_27, OpenJDK Runtime Environment
  • Glucose version 2.1 with SatELite preprocessor (64 bit code)
  • PBSugar version 1.1.1 with default encoding options:
    • sort=d : sort terms with the descending order of coefficients
    • clause : extract clause part from PB constraint
    • cnf=3 : translate directly to CNF by order encoding for the PB constraints containing at most 3 literals
    • decomp=100 : try decomposition of PB constraints for the base up to 100
    • axioms : generate axiom clauses
    • cache : use "reusing cache" of counter matrices
    • share=4 : try to share counter matrices when the length is greater than or equal to 4

Benchmark Instances

  • Download pb-dsl-list.csv.
    • NAME : Name of the instance
    • FAMILY : Name of the family
    • VARS : Number of variables
    • PBS : Number of PB constraints
    • FILE : File name of the instance
Family#InstancesAvg #VarsAvg #Constraints
lopes200475391095387
army12348643
blast837607763
cache963418185607
chnl212290125
dbstv3051600328901
dbstv4052800990001
dbstv50545002559501
dlx3767421764
elf51659347846
fpga36933687
j1202831469104663
j3017429613955
j6018955031142
j90171552450891
neos458465283
ooo193476899704
pig-card204015113
pig-cl204015161208
ppp6462930870
robin68876761
13queen100169101
11tsp111002312707
vdw52472276818
Total19003376878
  • There are 669 instances in 22 families. The family classification is given by {AbioNORM12}.
  • The following 7 instances are included in "lopes" family as classified in {AbioNORM12}.
    • normalized-1096.cudf.paranoid.opb
    • normalized-22s.smv.opb lopes
    • normalized-25s.smv.opb lopes
    • normalized-37s.smv.opb lopes
    • normalized-43s.smv.opb lopes
    • normalized-44s.smv.opb lopes
    • normalized-46s.smv.opb lopes
  • The name of 5 instances are renamed as used in {AbioNORM12}.
    • normalized-ppp:1,3-13,19.opb is renamed to normalized-ppp1-3-13-19.opb.
    • normalized-ppp:1-11,19,21.opb is renmaed to normalized-ppp1-11-19-21.opb.
    • normalized-ppp:1-12,16.opb is renmaed to normalized-ppp1-12-16.opb.
    • normalized-ppp:1-9,16-19.opb is renmaed to normalized-ppp1-9-16-19.opb.
    • normalized-ppp:3-13,25,26.opb is renmaed to normalized-ppp3-13-25-26.opb.

Results on Solving

Number of instances solved

FamilyVBSPBSugarSat4jclaspbsolowboMiniSat+
lopes (200)86814467366564
army (12)118510656
blast (8)8888888
cache (9)9969668
chnl (21)2162132133
dbstv30 (5)5555555
dbstv40 (5)5555555
dbstv50 (5)5555555
dlx (3)3333333
elf (5)5555555
fpga (36)36363634363633
j120 (28)16151516131512
j30 (17)17171717171717
j60 (18)17171717171717
j90 (17)17171717171717
neos (4)2222222
ooo (19)18151517121616
pig-card (20)2022021922
pig-cl (20)2222222
ppp (6)5443434
robin (6)4344333
13queen (100)100100100100100100100
11tsp11 (100)1001001001008510095
vdw (5)3212111
Total (669)515467457453428441433
  • This table shows the number of solved instances within the time limit (1000 seconds).

Time spent for solving

FamilyVBSPBSugarSat4jclaspbsolowboMiniSat+
lopes (200)638657844727847746752
army (12)218359603281565638506
blast (8)08310000
cache (9)117141346164395338221
chnl (21)076118630892861
dbstv30 (5)118682418
dbstv40 (5)2451247163213
dbstv50 (5)6107291231876102
dlx (3)0630200
elf (5)08401810
fpga (36)0316002114
j120 (28)442491489448537474572
j30 (17)01040402
j60 (18)56666056605662
j90 (17)01430001
neos (4)500526523503656500730
ooo (19)140275343180384258244
pig-card (20)2900390362915903
pig-cl (20)901913948904921939901
ppp (6)203340336501336500428
robin (6)334505346334517507533
13queen (100)056024285
11tsp11 (100)71880742860151
vdw (5)490695802620825801801
Average (669)260336357352421379412
  • This table shows the average time spent for solving (in seconds). Time spent for encoding is included.
  • Timeouts and memory overs are counted as 1000 seconds in the average computation.

Cactus Plot

cactus.png

cactus2.png

Enlarged plot from 300 instances to 500 instances

Effect of Reusing/Sharing Counter Matrices

When the reusing/sharing of Counter Matrices is disabled, the performance is declined.

  • PBSugar: default setting
  • PBSugar-Noreuse: "-o no_cache,share=0" option is set

Number of instances solved

FamilyPBSugarPBSugar-Noreuse
lopes (200)8181
army (12)88
blast (8)87
cache (9)97
chnl (21)66
dbstv30 (5)55
dbstv40 (5)55
dbstv50 (5)55
dlx (3)33
elf (5)55
fpga (36)3636
j120 (28)1515
j30 (17)1717
j60 (18)1717
j90 (17)1717
neos (4)22
ooo (19)1513
pig-card (20)22
pig-cl (20)22
ppp (6)44
robin (6)33
13queen (100)100100
11tsp11 (100)100100
vdw (5)22
Total (669)467462

Time spent for solving

FamilyPBSugarPBSugar-Noreuse
lopes (200)657657
army (12)359360
blast (8)83206
cache (9)141276
chnl (21)761761
dbstv30 (5)1826
dbstv40 (5)4560
dbstv50 (5)107147
dlx (3)67
elf (5)812
fpga (36)33
j120 (28)491491
j30 (17)1010
j60 (18)6667
j90 (17)1414
neos (4)526513
ooo (19)275342
pig-card (20)900900
pig-cl (20)913913
ppp (6)340340
robin (6)505505
13queen (100)55
11tsp11 (100)1818
vdw (5)695695
Average (669)336341

Raw Data

  • PBSugar: pbsugar-dsl-results.csv
    • PB : File name of the PB instance
    • FAMILY : Family name of the PB instance
    • VARS : Number of PB variables
    • PBS : Number of PB constraints
    • FIN : Finished (FIN), Timeout (TO), Memory over (MO)
      • Time limit is 1000 seconds
    • RESULT : Satisfiable (SAT), Unsatisfiable (UNSAT), Unknown (UNK)
    • CPU : Total CPU time in seconds
    • ENCODE_CPU : CPU time spent for encoding in seconds
    • SAT_CPU : CPU time spent by SAT solver in seconds
    • CM : Number of Counter Matrices constructed
    • REUSED : Number of times Counter Matrices reused
    • SHARED : Number of times Counter Matrices shared
    • DECOMP : Number of times PB constraits decomposed
    • SAT_VARS : Number of SAT variables
    • SAT_CLAUSES : Number of SAT clauses
  • Other solvers executed on our environment: pbother-dsl-results.csv
    • PB : File name of the PB instance
    • SOLVER : Solver name
    • FIN : Finished (FIN), Timeout (TO), Memory over (MO)
      • Time limit is 1000 seconds
    • RESULT : Satisfiable (SAT), Unsatisfiable (UNSAT), Unknown (UNK)
    • CPU : Total CPU time in seconds

Table of PBSugar Raw Data

PBFAMILYVARSPBSFINRESULTCPUENCODE_CPUSAT_CPUCMREUSEDSHAREDDECOMPSAT_VARSSAT_CLAUSES
normalized-01.opblopes9057194925FINSAT145.5114.66130.7070300019698278033
normalized-02.opblopes7069151430FINUNSAT92.3112.4179.7754600015328215936
normalized-03.opblopes8412181707FINSAT48.0514.2933.5865500018321259182
normalized-04.opblopes6426138234FINUNSAT33.2211.6121.4949800013953197107
normalized-05.opblopes7351155824FINSAT258.3113.13245.0556300015883222262
normalized-06.opblopes316467146FINSAT9.598.540.98242000682795793
normalized-07.opblopes7175155089FINSAT22.0612.659.2755900015632221243
normalized-08.opblopes5191111638FINUNSAT15.7310.615.0240200011266159190
normalized-09.opblopes5398114743FINUNSAT24.9010.2914.5141500011686163753
normalized-100.opblopes10086226240TOUNKT13.08T72000021738318834
normalized-101.opblopes7936176837FINUNSAT75.4311.3263.9856300017045249176
normalized-102.opblopes12587283937TOUNKT16.24T90300027198400140
normalized-103.opblopes10086226240TOUNKT13.09T72000021738318834
normalized-104.opblopes16024353350FINSAT44.7022.1822.25126100034978502721
normalized-105.opblopes33731740544TOUNKT39.58T2643000735111053242
normalized-106.opblopes39025858412TOUNKT46.54T3062000850961220734
normalized-107.opblopes10238224043FINSAT23.9116.457.2980000022271318813
normalized-108.opblopes33731740544TOUNKT39.79T2643000735111053242
normalized-1096.cudf.paranoid.opblopes11FINSAT0.160.070.07000011
normalized-109.opblopes11274247096FINSAT25.0315.359.4988200024537351583
normalized-10.opblopes7880170354FINSAT39.2013.5125.5561400017168242998
normalized-110.opblopes39025858412TOUNKT46.12T3062000850961220734
normalized-111.opblopes33692740354TOUNKT39.65T2642000734511052961
normalized-112.opblopes33692740354TOUNKT39.67T2642000734511052961
normalized-113.opblopes8316181309FINSAT19.8114.145.5264800018069258067
normalized-114.opblopes28939633938TOUNKT35.52T226400063028901752
normalized-115.opblopes16024353350FINSAT44.4623.2120.97126100034978502721
normalized-116.opblopes44846988104TOUNKT52.61T3523000978381405027
normalized-117.opblopes10238224043FINSAT28.7515.6312.9580000022271318813
normalized-118.opblopes11274247096FINSAT27.4017.539.6988200024537351583
normalized-119.opblopes484111121517TOUNKT58.71T35230001049501575406
normalized-11.opblopes5895126892FINUNSAT22.0411.4710.4445700012801180934
normalized-120.opblopes484111121517TOUNKT59.95T35230001049501575406
normalized-121.opblopes552961282690TOUNKT66.55T40300001199781801984
normalized-122.opblopes484111121517TOUNKT59.70T35230001049501575406
normalized-123.opblopes36611853935FINSAT532.5645.95485.972685000796681200159
normalized-124.opblopes29741692942FINUNSAT575.1140.40534.13217800064655973761
normalized-125.opblopes553011282592TOUNKT67.55T40320001200391802175
normalized-126.opblopes484171121431TOUNKT59.65T35250001050121575609
normalized-127.opblopes484111121517TOUNKT59.73T35230001049501575406
normalized-128.opblopes467331087391TOUNKT63.30T34170001015341527780
normalized-129.opblopes483681121286TOUNKT59.25T35220001048841575075
normalized-12.opblopes352875039FINSAT10.719.161.482710007632107095
normalized-130.opblopes41972972388TOUNKT50.85T3056000910181366121
normalized-131.opblopes21928509638FINUNSAT153.1330.46122.27160200047612716211
normalized-132.opblopes551361280712TOUNKT67.66T40240001197081799290
normalized-133.opblopes482531119563TOUNKT58.56T35170001046821572736
normalized-134.opblopes484111121517TOUNKT59.21T35230001049501575406
normalized-135.opblopes552961282690TOUNKT68.76T40300001199781801984
normalized-136.opblopes484111121517TOUNKT59.05T35230001049501575406
normalized-137.opblopes484111121517TOUNKT59.78T35230001049501575406
normalized-138.opblopes483681121286TOUNKT59.20T35220001048841575075
normalized-139.opblopes35834835510FINSAT312.9548.46263.862626000779301174063
normalized-13.opblopes6737135818FINSAT50.279.3840.7856200014673196273
normalized-140.opblopes477591109809TOUNKT58.63T34870001036941559170
normalized-141.opblopes42085974087TOUNKT50.55T3061000912181368436
normalized-142.opblopes482601119489TOUNKT59.56T35190001047451572951
normalized-143.opblopes41972972388TOUNKT51.24T3056000910181366121
normalized-144.opblopes552961282690TOUNKT68.65T40300001199781801984
normalized-145.opblopes484111121517TOUNKT59.16T35230001049501575406
normalized-146.opblopes484171121431TOUNKT59.42T35250001050121575609
normalized-147.opblopes42127974306TOUNKT52.57T3062000912831368755
normalized-148.opblopes482531119563TOUNKT59.25T35170001046821572736
normalized-149.opblopes542061261615TOUNKT72.83T39650001178131772669
normalized-14.opblopes5911120546FINSAT13.908.515.2649800012931174193
normalized-150.opblopes473261100502TOUNKT65.70T34580001027901546151
normalized-151.opblopes42127974306TOUNKT51.12T3062000912831368755
normalized-152.opblopes29741692942FINSAT188.9337.09151.33217800064655973761
normalized-153.opblopes552961282690TOUNKT69.08T40300001199781801984
normalized-154.opblopes484111121517TOUNKT59.46T35230001049501575406
normalized-155.opblopes40423942446TOUNKT53.11T2962000879091324285
normalized-156.opblopes38303893113FINSAT478.8951.29426.932807000833021254986
normalized-157.opblopes41972972388TOUNKT51.22T3056000910181366121
normalized-158.opblopes1132122516734TOUNKT137.51T89570002477503577421
normalized-159.opblopes1024492274228TOUNKT124.76T80940002240483232622
normalized-15.opblopes6809146226FINSAT20.6312.667.8552700014777208508
normalized-160.opblopes1133862518744TOUNKT140.20T89630002480263580087
normalized-161.opblopes1348423153398TOUNKT174.59T98860002932384427911
normalized-162.opblopes26339612374FINSAT101.7132.5568.69192200057129860285
normalized-163.opblopes1350273155676TOUNKT174.75T98920002935334430905
normalized-164.opblopes26339612374FINSAT122.3035.8885.96192200057129860285
normalized-165.opblopes1477643459649TOUNKT202.08T108470003215294858160
normalized-166.opblopes26339612374FINSAT102.1835.8065.93192200057129860285
normalized-167.opblopes1061962493137TOUNKT148.51T78230002314653502016
normalized-168.opblopes1286663016254TOUNKT180.26T94620002802224236303
normalized-169.opblopes1484863472197TOUNKT191.58T108830003228554875236
normalized-16.opblopes11658250186FINSAT856.6015.20841.2090300025344356909
normalized-170.opblopes26339612374FINSAT110.4036.9473.00192200057129860285
normalized-171.opblopes1224072858957TOUNKT157.03T89630002660424014374
normalized-172.opblopes2880806434441TOUNKT431.56T228860006316079145467
normalized-173.opblopes2682415985144TOUNKT351.55T212830005877418506132
normalized-174.opblopes2486595546518TOUNKT326.86T197240005447687882792
normalized-175.opblopes2486595546518TOUNKT325.19T197240005447687882792
normalized-176.opblopes3105717294179TOUNKT472.29T2285700067655210241748
normalized-177.opblopes605361417665FINSAT792.5881.95709.5944470001317331991272
normalized-178.opblopes3343697853489TOUNKT509.70T2460700072836411026750
normalized-179.opblopes3118277317246TOUNKT443.32T2292200067888310273055
normalized-17.opblopes9342199352TOUNKT12.32T72000020256284392
normalized-180.opblopes3118277317246TOUNKT429.19T2292200067888310273055
normalized-181.opblopes3351617866877TOUNKT465.69T2464300072976011044666
normalized-182.opblopes59952714097016TOUNKT875.45T44152000130633319791205
normalized-183.opblopes59952714097016TOUNKT890.69T44152000130633319791205
normalized-184.opblopes102512724132986TOUNKTTTTTTTTT
normalized-185.opblopes184046243FINSAT25.266.6818.5473000394962686
normalized-186.opblopes110324920FINUNSAT118.426.46111.9342000237034392
normalized-187.opblopes150833299FINSAT4.934.290.6173000325746610
normalized-188.opblopes4838027FINUNSAT2.772.380.3721000103811851
normalized-189.opblopes14685417306TOUNKT20.40T73000031195557479
normalized-18.opblopes9342199352FINSAT122.6812.59109.9072000020256284392
normalized-190.opblopes11586326275TOUNKT16.23T57300024587436275
normalized-191.opblopes22941594926TOUNKT29.78T135900049143812886
normalized-192.opblopes15414395824TOUNKT20.37T90700032942541207
normalized-193.opblopes12360315408TOUNKT16.46T72400026368431404
normalized-19.opblopes7351155824FINUNSAT512.3810.38501.8856300015883222262
normalized-20.opblopes9342199352FINSAT317.2812.46304.6672000020256284392
normalized-21.opblopes7351155824FINUNSAT354.1013.43340.5556300015883222262
normalized-22.opblopes9355199372TOUNKT12.38T72200020320284674
normalized-22s.smv.opblopes598515365FINUNSAT13.859.114.73632720003264091446845
normalized-23.opblopes7365155855TOUNKT10.47T56500015948222555
normalized-24.opblopes9342199352TOUNKT12.18T72000020256284392
normalized-25.opblopes7351155824FINUNSAT184.2110.36173.7256300015883222262
normalized-25s.smv.opblopes507212829FINUNSAT11.938.293.61514594002656701177039
normalized-26.opblopes7351155824FINSAT193.139.96183.0556300015883222262
normalized-27.opblopes9355199372TOUNKT12.88T72200020320284674
normalized-28.opblopes7365155855TOUNKT10.14T56500015948222555
normalized-29.opblopes9220197914FINSAT294.6912.94281.5871400020032282298
normalized-30.opblopes7231154408FINUNSAT55.749.8245.7955700015661220190
normalized-31.opblopes9310199239FINSAT404.6512.02392.4771900020203284188
normalized-32.opblopes7320155722FINUNSAT210.8710.25200.4956200015831222069
normalized-33.opblopes7085151483FINSAT112.6511.39101.1154800015395216251
normalized-34.opblopes5398114743FINUNSAT34.5411.3323.0941500011686163753
normalized-35.opblopes9220197914FINSAT109.1511.9797.0371400020032282298
normalized-36.opblopes7231154408FINUNSAT84.9310.7574.0655700015661220190
normalized-37.opblopes9310199239FINSAT556.4012.30543.9571900020203284188
normalized-37s.smv.opblopes11903183FINUNSAT3.012.800.192410400414216167
normalized-38.opblopes7320155722FINUNSAT51.6210.1941.2956200015831222069
normalized-39.opblopes11658250186TOUNKT15.11T90300025344356909
normalized-40.opblopes9342199352TOUNKT11.71T72000020256284392
normalized-41.opblopes5690119124FINSAT84.618.5875.9343400012302170328
normalized-42.opblopes427688544FINUNSAT33.436.9326.423230009196126597
normalized-43.opblopes7175155089FINSAT22.2212.839.2355900015632221243
normalized-43s.smv.opblopes36558686FINUNSAT9.296.352.9232438000167893742414
normalized-44.opblopes5191111638FINUNSAT16.8910.456.3540200011266159190
normalized-44s.smv.opblopes495940FINUNSAT4.604.330.256476001654572240
normalized-45.opblopes428991910FINSAT10.969.571.313310009293131076
normalized-46.opblopes12552283802TOUNKT15.44T90200027140399905
normalized-46s.smv.opblopes16123653FINUNSAT6.245.610.611662140043278188743
normalized-47.opblopes10052226117TOUNKT13.31T71900021681318611
normalized-48.opblopes9956224622FINSAT352.5713.16339.2371400021498316500
normalized-49.opblopes7808175243FINUNSAT72.3711.4060.8355700016807246866
normalized-50.opblopes10086226240TOUNKT13.66T72000021738318834
normalized-51.opblopes7936176837FINUNSAT55.6811.7443.7956300017045249176
normalized-52.opblopes12587283937TOUNKT15.89T90300027198400140
normalized-53.opblopes10086226240TOUNKT13.99T72000021738318834
normalized-54.opblopes10086226240FINSAT597.5713.62583.7972000021738318834
normalized-55.opblopes7936176837FINUNSAT183.8210.75172.9356300017045249176
normalized-56.opblopes15466350566TOUNKT19.21T111400033484493990
normalized-57.opblopes12587283937TOUNKT16.52T90300027198400140
normalized-58.opblopes12587283937TOUNKT16.33T90300027198400140
normalized-59.opblopes10086226240TOUNKT12.79T72000021738318834
normalized-60.opblopes12587283937TOUNKT17.18T90300027198400140
normalized-61.opblopes10086226240TOUNKT13.40T72000021738318834
normalized-62.opblopes12587283937TOUNKT16.83T90300027198400140
normalized-63.opblopes10086226240TOUNKT13.83T72000021738318834
normalized-64.opblopes12587283937TOUNKT16.45T90300027198400140
normalized-65.opblopes10086226240TOUNKT13.24T72000021738318834
normalized-66.opblopes12587283937TOUNKT16.52T90300027198400140
normalized-67.opblopes10086226240TOUNKT13.65T72000021738318834
normalized-68.opblopes12552283802TOUNKT15.56T90200027140399905
normalized-69.opblopes10052226117TOUNKT12.87T71900021681318611
normalized-70.opblopes12552283802TOUNKT15.53T90200027140399905
normalized-71.opblopes10052226117TOUNKT13.34T71900021681318611
normalized-72.opblopes10086226240TOUNKT13.42T72000021738318834
normalized-73.opblopes7936176837FINUNSAT415.6411.71403.7956300017045249176
normalized-74.opblopes12587283937TOUNKT15.92T90300027198400140
normalized-75.opblopes10086226240TOUNKT13.76T72000021738318834
normalized-76.opblopes12587283937TOUNKT16.26T90300027198400140
normalized-77.opblopes10086226240TOUNKT13.44T72000021738318834
normalized-78.opblopes15430350419TOUNKT19.34T111300033425493743
normalized-79.opblopes12552283802TOUNKT16.73T90200027140399905
normalized-80.opblopes12587283937TOUNKT16.55T90300027198400140
normalized-81.opblopes10086226240TOUNKT13.23T72000021738318834
normalized-82.opblopes12455282295TOUNKT16.11T89700026956397782
normalized-83.opblopes9956224622TOUNKT13.44T71400021498316500
normalized-84.opblopes6426138234FINUNSAT25.9511.5114.3349800013953197107
normalized-85.opblopes9500215324FINSAT151.0615.38135.4668400020548303390
normalized-86.opblopes7354165969FINUNSAT33.1113.0519.9252700015859233780
normalized-87.opblopes6368144031FINUNSAT18.9712.106.7545700013739202870
normalized-88.opblopes12587283937TOUNKT16.77T90300027198400140
normalized-89.opblopes10086226240TOUNKT13.84T72000021738318834
normalized-90.opblopes12587283937TOUNKT15.88T90300027198400140
normalized-91.opblopes10086226240TOUNKT13.64T72000021738318834
normalized-92.opblopes9086206245FINSAT283.5715.47267.9565500019663290599
normalized-93.opblopes6941156902FINUNSAT44.1412.4831.5549800014975221001
normalized-94.opblopes12587283937TOUNKT16.94T90300027198400140
normalized-95.opblopes10086226240TOUNKT13.31T72000021738318834
normalized-96.opblopes12587283937TOUNKT16.70T90300027198400140
normalized-97.opblopes10086226240TOUNKT13.27T72000021738318834
normalized-98.opblopes10052226117FINSAT778.2412.38765.6871900021681318611
normalized-99.opblopes7903176726FINUNSAT46.6110.8735.6056200016989248965
normalized-army10.14bt.opbarmy316686FINSAT24.622.8021.809101431520502
normalized-army10.14ls.opbarmy316476FINSAT4.632.002.612000310614766
normalized-army11.17bt.opbarmy370809TOUNKT3.06T9101562926997
normalized-army11.17ls.opbarmy370557FINSAT14.072.2411.812000442021219
normalized-army12.21bt.opbarmy428942TOUNKT2.83T9101876242144
normalized-army12.21ls.opbarmy428644TOUNKT2.76T2000630230502
normalized-army13.24bt.opbarmy4901085TOUNKT3.51T91011080052255
normalized-army13.24ls.opbarmy490737FINSAT243.463.03240.412000834040563
normalized-army8.9bt.opbarmy220470FINSAT2.061.890.15910119929256
normalized-army8.9ls.opbarmy220332FINSAT2.841.451.37200014106498
normalized-army9.12bt.opbarmy266573FINSAT3.272.430.819101279813215
normalized-army9.12ls.opbarmy266401FINSAT12.511.6810.812000221610423
normalized-blast-floppy1-2.ucl.opbblast152127FINUNSAT4.604.150.4326240039206175417
normalized-blast-floppy1-3.ucl.opbblast274259FINUNSAT3.873.730.124753001109948326
normalized-blast-floppy1-4.ucl.opbblast237197FINUNSAT3.463.280.1638360032763146011
normalized-blast-floppy1-6.ucl.opbblast719593FINUNSAT8.846.961.8610711500190830854096
normalized-blast-floppy1-7.ucl.opbblast29133105FINUNSAT219.35212.307.0341143500583644426244010
normalized-blast-floppy1-8.ucl.opbblast36183931FINUNSAT304.91295.609.2952154500799846535967700
normalized-blast-tlan2.ucl.opbblast22213050FINUNSAT18.2214.723.48357363007264143254775
normalized-blast-tlan3.ucl.opbblast1994450842FINUNSAT97.5693.284.223470347400709993231839856
normalized-cache-ibm-q-full.all.ucl.opbcache81558240469FINUNSAT363.7817.96345.6121282476006153862611941
normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opbcache87751254772FINUNSAT51.0932.1518.75324744650015008186562585
normalized-cache-ibm-q-unbounded.Icl2arity.ucl.opbcache2383767568FINUNSAT16.6610.606.0013351835003115121343807
normalized-cache-ibm-q-unbounded.Ih1arity.ucl.opbcache201731592525FINUNSAT662.8260.62601.785258783800254261511043059
normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opbcache76091218262FINSAT42.7137.085.42445162010020067488836439
normalized-cache.inv10.ucl.opbcache893726319FINUNSAT5.504.860.60136136001696160999
normalized-cache.inv12.ucl.opbcache2580076699FINUNSAT8.797.321.411901900037010125149
normalized-cache.inv14.ucl.opbcache62704187107FINUNSAT132.1312.29119.702522520093700323439
normalized-cache.inv8.ucl.opbcache23556744FINUNSAT4.704.460.22888800754729184
normalized-chnl10_11_pb.cnf.cr.opbchnl22042FINUNSAT1.000.670.31200006401842
normalized-chnl10_15_pb.cnf.cr.opbchnl30050FINUNSAT1.120.540.55200008802570
normalized-chnl10_20_pb.cnf.cr.opbchnl40060FINUNSAT1.420.770.632000011803480
normalized-chnl15_16_pb.cnf.cr.opbchnl48062FINUNSAT393.351.63391.693000014104112
normalized-chnl15_20_pb.cnf.cr.opbchnl60070FINUNSAT328.110.89327.193000017705200
normalized-chnl15_25_pb.cnf.cr.opbchnl75080FINUNSAT267.752.36265.373000022206560
normalized-chnl20_21_pb.cnf.cr.opbchnl84082TOUNKT2.60T4000024807282
normalized-chnl20_25_pb.cnf.cr.opbchnl100090TOUNKT2.66T4000029608730
normalized-chnl20_30_pb.cnf.cr.opbchnl1200100TOUNKT2.90T40000356010540
normalized-chnl30_31_pb.cnf.cr.opbchnl1860122TOUNKT3.44T60000552016322
normalized-chnl30_35_pb.cnf.cr.opbchnl2100130TOUNKT3.08T60000624018490
normalized-chnl30_40_pb.cnf.cr.opbchnl2400140TOUNKT2.88T60000714021200
normalized-chnl35_36_pb.cnf.cr.opbchnl2520142TOUNKT1.68T70000749022192
normalized-chnl35_40_pb.cnf.cr.opbchnl2800150TOUNKT4.26T70000833024720
normalized-chnl35_45_pb.cnf.cr.opbchnl3150160TOUNKT2.82T70000938027880
normalized-chnl40_41_pb.cnf.cr.opbchnl3280162TOUNKT2.00T80000976028962
normalized-chnl40_45_pb.cnf.cr.opbchnl3600170TOUNKT4.60T800001072031850
normalized-chnl40_50_pb.cnf.cr.opbchnl4000180TOUNKT2.73T800001192035460
normalized-chnl50_51_pb.cnf.cr.opbchnl5100202TOUNKT3.32T1000001520045202
normalized-chnl50_55_pb.cnf.cr.opbchnl5500210TOUNKT3.60T1000001640048810
normalized-chnl50_60_pb.cnf.cr.opbchnl6000220TOUNKT3.45T1000001790053320
normalized-dbst_v30_e350_d15_mw10_1.opb.PB06.opbdbstv301600328901FINSAT17.7115.971.4612117100041675523357
normalized-dbst_v30_e350_d15_mw10_2.opb.PB06.opbdbstv301600328901FINSAT17.4815.771.4812117100041555522757
normalized-dbst_v30_e350_d15_mw10_3.opb.PB06.opbdbstv301600328901FINSAT18.0116.311.4712117100041334521652
normalized-dbst_v30_e350_d15_mw10_8.opb.PB06.opbdbstv301600328901FINSAT17.7016.021.4612117100042157525767
normalized-dbst_v30_e350_d15_mw10_9.opb.PB06.opbdbstv301600328901FINSAT16.4614.681.5612117100041253521247
normalized-dbst_v40_e600_d20_mw10_0.opb.PB06.opbdbstv402800990001FINSAT43.8339.423.74161308000947681439682
normalized-dbst_v40_e600_d20_mw10_2.opb.PB06.opbdbstv402800990001FINSAT44.7940.263.89161308000928051429867
normalized-dbst_v40_e600_d20_mw10_5.opb.PB06.opbdbstv402800990001FINSAT44.1139.573.88161308000937081434382
normalized-dbst_v40_e600_d20_mw10_6.opb.PB06.opbdbstv402800990001FINSAT44.1139.603.85161308000933061432372
normalized-dbst_v40_e600_d20_mw10_9.opb.PB06.opbdbstv402800990001FINSAT41.8437.343.87161308000943111437397
normalized-dbst_v50_e1000_d25_mw10_1.opb.PB06.opbdbstv5045002559501FINSAT107.7396.769.352014850001929583485592
normalized-dbst_v50_e1000_d25_mw10_3.opb.PB06.opbdbstv5045002559501FINSAT106.2795.029.452014850001922223481912
normalized-dbst_v50_e1000_d25_mw10_5.opb.PB06.opbdbstv5045002559501FINSAT103.1692.119.412014850001910053475827
normalized-dbst_v50_e1000_d25_mw10_6.opb.PB06.opbdbstv5045002559501FINSAT104.6893.529.592014850001914193477897
normalized-dbst_v50_e1000_d25_mw10_9.opb.PB06.opbdbstv5045002559501FINSAT105.7194.829.312014850001919113480357
normalized-dlx1c.rwmem1.ucl.opbdlx757821401FINUNSAT5.153.971.153865140050448209635
normalized-dlx1c.rwmem.ucl.opbdlx905125833FINUNSAT5.474.201.233825100051685213047
normalized-dlx1c.ucl.opbdlx639218058FINUNSAT4.743.750.963264540045466189848
normalized-elf.rf10.ucl.opbelf55066160619FINUNSAT19.1413.105.8913612671003810511608234
normalized-elf.rf6.ucl.opbelf67132FINUNSAT0.360.260.084800175584
normalized-elf.rf7.ucl.opbelf13283349FINUNSAT4.764.530.216611800791032191
normalized-elf.rf8.ucl.opbelf605916684FINUNSAT6.085.260.802864580040565168414
normalized-elf.rf9.ucl.opbelf2044558444FINUNSAT9.216.582.58696132800169033717452
normalized-fpga10_10_sat_pb.cnf.cr.opbfpga150130FINSAT0.790.670.11200004301300
normalized-fpga10_8_sat_pb.cnf.cr.opbfpga120106FINSAT0.430.320.09180003421024
normalized-fpga10_9_sat_pb.cnf.cr.opbfpga135118FINSAT0.630.540.07190003861162
normalized-fpga11_10_sat_pb.cnf.cr.opbfpga165141FINSAT1.020.890.11210004741437
normalized-fpga11_11_sat_pb.cnf.cr.opbfpga182154FINSAT1.040.900.12220005241594
normalized-fpga11_9_sat_pb.cnf.cr.opbfpga149128FINSAT0.510.380.11200004271289
normalized-fpga12_10_sat_pb.cnf.cr.opbfpga180152FINSAT1.211.080.11220005181574
normalized-fpga12_11_sat_pb.cnf.cr.opbfpga198166FINSAT1.261.110.13230005711741
normalized-fpga12_12_sat_pb.cnf.cr.opbfpga216180FINSAT1.441.170.25240006241908
normalized-fpga13_11_sat_pb.cnf.cr.opbfpga215178FINSAT1.251.120.11240006211897
normalized-fpga13_12_sat_pb.cnf.cr.opbfpga234193FINSAT1.501.370.11250006772074
normalized-fpga13_13_sat_pb.cnf.cr.opbfpga254208FINSAT1.601.460.12260007362260
normalized-fpga14_12_sat_pb.cnf.cr.opbfpga252206FINSAT1.501.370.11260007302240
normalized-fpga14_13_sat_pb.cnf.cr.opbfpga273222FINSAT1.631.460.14270007922436
normalized-fpga14_14_sat_pb.cnf.cr.opbfpga294238FINSAT0.950.800.13280008542632
normalized-fpga15_13_sat_pb.cnf.cr.opbfpga293236FINSAT1.871.720.12280008512621
normalized-fpga15_14_sat_pb.cnf.cr.opbfpga315253FINSAT1.941.770.15290009162827
normalized-fpga15_15_sat_pb.cnf.cr.opbfpga338270FINSAT2.242.070.15300009843042
normalized-fpga20_18_sat_pb.cnf.cr.opbfpga540416FINSAT3.072.820.233800015824934
normalized-fpga20_19_sat_pb.cnf.cr.opbfpga570438FINSAT3.253.070.163900016715217
normalized-fpga20_20_sat_pb.cnf.cr.opbfpga600460FINSAT3.383.040.324000017605500
normalized-fpga25_23_sat_pb.cnf.cr.opbfpga863646FINSAT3.963.730.204800025417981
normalized-fpga25_24_sat_pb.cnf.cr.opbfpga900673FINSAT4.053.790.244900026518332
normalized-fpga25_25_sat_pb.cnf.cr.opbfpga938700FINSAT4.334.060.255000027648692
normalized-fpga30_28_sat_pb.cnf.cr.opbfpga1260926FINSAT4.404.100.2858000372211744
normalized-fpga30_29_sat_pb.cnf.cr.opbfpga1305958FINSAT5.024.300.7059000385612172
normalized-fpga30_30_sat_pb.cnf.cr.opbfpga1350990FINSAT5.124.700.4060000399012600
normalized-fpga35_33_sat_pb.cnf.cr.opbfpga17331256FINSAT3.623.170.4368000513116241
normalized-fpga35_34_sat_pb.cnf.cr.opbfpga17851293FINSAT7.195.002.1769000528616737
normalized-fpga35_35_sat_pb.cnf.cr.opbfpga18381330FINSAT13.085.018.0570000544417242
normalized-fpga40_38_sat_pb.cnf.cr.opbfpga22801636FINSAT3.523.130.3778000676221454
normalized-fpga40_39_sat_pb.cnf.cr.opbfpga23401678FINSAT5.505.100.3879000694122027
normalized-fpga40_40_sat_pb.cnf.cr.opbfpga24001720FINSAT5.585.140.4280000712022600
normalized-fpga45_43_sat_pb.cnf.cr.opbfpga29032066FINSAT4.273.780.4788000862127401
normalized-fpga45_44_sat_pb.cnf.cr.opbfpga29702113FINSAT6.413.782.6189000882128042
normalized-fpga45_45_sat_pb.cnf.cr.opbfpga30382160FINSAT4.933.881.0290000902428692
normalized-j12010_10-sat.opbj1201621450734FINSAT16.2710.006.222640005929222892364
normalized-j12013_1-unsat.opbj1202928292908FINUNSAT16.4515.191.184800009424824586668
normalized-j12015_3-unsat.opbj1202105466352FINUNSAT15.4214.221.1234400010349085074734
normalized-j1201_5-sat.opbj1202734686712FINSAT9.686.812.81448000138002614008
normalized-j12016_4-sat.opbj12048642155800TOUNKT23.50T80000014584427074000
normalized-j12021_4-sat.opbj12032912109489FINSAT14.629.644.89540000158732706999
normalized-j12022_9-sat.opbj1202662088108FINSAT11.018.392.54436000154259698617
normalized-j12023_3-unsat.opbj1202395879333FINUNSAT9.138.460.61392000166842767685
normalized-j12026_5-unsat.opbj12032912109848FINUNSAT405.3011.21393.995400003400371595388
normalized-j12027_7-unsat.opbj1202758891561FINUNSAT29.5810.7218.764520003763061790064
normalized-j12032_3-unsat.opbj12032186107047TOUNKT14.72T5280008210183977815
normalized-j12032_8-unsat.opbj12031460104814TOUNKT14.66T5160007947533849555
normalized-j1203_2-sat.opbj1202153867936FINSAT9.907.592.25352000149930686488
normalized-j12033_3-sat.opbj1202613686824TOUNKT14.15T4280008545304163738
normalized-j12034_4-sat.opbj1202323276633FINSAT42.1914.8227.3138000011186775487548
normalized-j12036_3-sat.opbj12055660186884TOUNKT25.00T91600014809567167262
normalized-j12036_4-sat.opbj12057354192702TOUNKT25.77T94400014089266800466
normalized-j12037_7-sat.opbj12039204130975TOUNKT21.46T64400014122126884603
normalized-j12038_8-unsat.opbj1202904096434TOUNKT17.35T47600014838157279393
normalized-j12041_4-unsat.opbj1202807297590FINUNSAT11.698.832.79460000130537584385
normalized-j12045_10-sat.opbj1202420083750FINSAT11.728.852.81396000185075858821
normalized-j12047_10-unsat.opbj12030492105829TOUNKT11.76T5000004377422090954
normalized-j1205_1-unsat.opbj1202226470239FINUNSAT9.048.340.64364000198076920543
normalized-j12052_5-unsat.opbj12037752131628TOUNKT16.10T6200008012823867748
normalized-j12056_10-unsat.opbj12057354201250TOUNKT25.43T94400013039066288162
normalized-j12058_4-sat.opbj12035332122962TOUNKT21.38T58000015420277552037
normalized-j1208_10-unsat.opbj1202202269222TOUNKT10.35T3600004811122321382
normalized-j1209_4-sat.opbj1202129666999FINSAT131.8210.16121.613480004703902270622
normalized-j301_4-unsat.opbj30384411854FINUNSAT4.604.290.291830001421457726
normalized-j3020_1-sat.opbj30359611581FINSAT5.444.880.542280002092489671
normalized-j3024_4-sat.opbj30334810816FINSAT5.754.830.9021200057408266435
normalized-j3025_1-sat.opbj30582819158FINSAT7.025.241.7537200072416333219
normalized-j3025_7-sat.opbj30595219548FINSAT7.695.492.1738000079482367153
normalized-j3027_8-sat.opbj30415413519FINSAT6.355.061.2626400085268400675
normalized-j3029_6-sat.opbj30576618893FINSAT27.855.8221.99368000119938566201
normalized-j3029_8-unsat.opbj30496016157FINUNSAT44.845.8139.00316000114217541270
normalized-j3031_7-sat.opbj30384412376FINSAT7.375.691.66244000132737636101
normalized-j3037_5-sat.opbj30502217060FINSAT6.225.260.9432000039502176420
normalized-j3041_4-unsat.opbj30483616649FINUNSAT6.125.031.0630800064588299470
normalized-j3046_4-unsat.opbj30396813430FINUNSAT7.496.131.33252000120203575831
normalized-j3048_8-sat.opbj3027909355FINSAT6.815.421.37176000120886582851
normalized-j308_1-unsat.opbj3027288382FINUNSAT5.204.950.2317200040267184596
normalized-j308_6-sat.opbj3029769039FINSAT5.454.600.8318800055099256353
normalized-j309_10-unsat.opbj30545617015FINUNSAT7.495.701.7634800074273342569
normalized-j309_9-sat.opbj30396812403FINSAT6.585.021.5425200054305250795
normalized-j6010_2-unsat.opbj60756423412FINUNSAT7.697.010.642440003267161588733
normalized-j6013_2-unsat.opbj601232238967TOUNKT8.78T4000003539221705167
normalized-j6015_4-sat.opbj60927228866FINSAT18.369.498.833000006579473224991
normalized-j6018_3-sat.opbj60951631278FINSAT6.795.631.1230800050403222161
normalized-j6022_1-sat.opbj60793025932FINSAT7.485.561.88256000137978655244
normalized-j6027_4-unsat.opbj60732023840FINUNSAT8.247.600.622360003306401610409
normalized-j602_7-unsat.opbj60646619939FINUNSAT5.514.960.5220800046714209947
normalized-j6030_9-unsat.opbj601195639426FINUNSAT10.629.780.803880005040372452883
normalized-j603_2-unsat.opbj60841826241FINUNSAT6.215.740.4427200062274280425
normalized-j6033_2-unsat.opbj601220042056FINUNSAT6.445.870.5339600052295226691
normalized-j6035_10-sat.opbj60878430004FINSAT6.695.521.1328400058058261464
normalized-j6040_1-sat.opbj601061436312FINSAT10.477.502.933440002443621171426
normalized-j6041_4-sat.opbj601634856848FINSAT18.846.8611.925320002554821211155
normalized-j6048_4-sat.opbj60768626213FINSAT14.959.145.772480005810002852731
normalized-j605_10-unsat.opbj60963830220FINUNSAT40.916.2734.60312000120632563896
normalized-j605_1-unsat.opbj60927229174FINUNSAT18.604.5813.98300000102947477974
normalized-j605_7-sat.opbj60927229130FINSAT8.175.532.6130000091772422955
normalized-j606_1-unsat.opbj60732022689FINUNSAT6.125.600.50236000129155612689
normalized-j9010_6-unsat.opbj901674452975FINUNSAT12.8211.731.043640007200833517527
normalized-j9010_8-sat.opbj901492446875FINSAT24.2810.3413.893240005573002715096
normalized-j9012_2-unsat.opbj901292240512FINUNSAT13.1111.921.1428000012587826203942
normalized-j9012_5-sat.opbj901528848064FINSAT18.5615.063.4433200014101036948352
normalized-j9014_1-unsat.opbj901619850975FINUNSAT15.4414.301.0835200011273745542439
normalized-j9015_10-unsat.opbj901419644553FINUNSAT15.4414.161.2230800012394206107225
normalized-j9027_5-sat.opbj901820060215FINSAT18.2211.646.523960009825594816571
normalized-j9028_2-unsat.opbj901383245398FINUNSAT13.8912.781.0730000010815325323823
normalized-j903_10-unsat.opbj901183036862FINUNSAT6.505.860.59256000114294530622
normalized-j9035_1-unsat.opbj901783661428FINUNSAT8.767.740.97388000155867724617
normalized-j9035_5-sat.opbj901892865252FINSAT9.717.412.24412000147060679544
normalized-j9039_3-unsat.opbj901510651849FINUNSAT9.338.520.763280004023921948673
normalized-j9042_5-sat.opbj901929266786FINSAT24.1811.7312.374200006638873235476
normalized-j9043_2-sat.opbj901674457767FINSAT19.8211.777.993640007596683717514
normalized-j9048_1-unsat.opbj901510651743FINUNSAT20.5818.911.6132800019683469733319
normalized-j906_2-sat.opbj901583449853FINSAT11.837.034.763440003617261741387
normalized-j907_8-unsat.opbj901092034033FINUNSAT7.266.480.742360004086981988644
normalized-neos808444.opbneos1984618245FINSAT13.157.835.27471700396217007909101
normalized-neos-820146.opbneos600830TOUNKT1.27T60450019656870
normalized-neos-820157.opbneos12001015TOUNKT1.64T854500417014315
normalized-neos-849702.opbneos17371041FINSAT91.605.1186.471041083051019223602
normalized-ooo.burch_dill.2.accl.ucl.opbooo21525613FINUNSAT4.453.460.97187289002152590586
normalized-ooo.burch_dill.3.accl.ucl.opbooo462212569FINUNSAT7.765.192.542925240035348147375
normalized-ooo.burch_dill.4.accl.ucl.opbooo393910412FINUNSAT6.045.240.781914810045138193169
normalized-ooo.burch_dill.6.accl.ucl.opbooo2362167526TOUNKT9.38T718168200182625773022
normalized-ooo.burch_dill.8.accl.ucl.opbooo2138060984FINUNSAT170.516.97163.48551160500143735603899
normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opbooo49621138346FINUNSAT233.7732.17201.48559953570020085008869651
normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opbooo109757313451TOUNKT61.41T90168506100408516518060817
normalized-ooo.ex.mem.LdValue.ucl.opbooo77106218779TOUNKT40.68T6748647200249177810983011
normalized-ooo.ex.mem.LsqHdStrong.ucl.opbooo168111487525TOUNKT67.85T9402939640405151517816785
normalized-ooo.rf10.ucl.opbooo1806952475FINUNSAT7.965.242.673975230066732266524
normalized-ooo.rf6.ucl.opbooo18044931FINUNSAT5.184.930.2210312100787131154
normalized-ooo.rf7.ucl.opbooo373610457FINUNSAT6.005.480.50166202002284894433
normalized-ooo.rf8.ucl.opbooo683219477FINUNSAT6.465.670.762322920033264135597
normalized-ooo.rf9.ucl.opbooo1147633090FINUNSAT5.594.451.103093990046373186377
normalized-ooo.tag10.ucl.opbooo907125914FINUNSAT7.015.701.272994250045680186945
normalized-ooo.tag12.ucl.opbooo2060559851FINUNSAT9.737.682.004806960079271317901
normalized-ooo.tag14.ucl.opbooo40605118930FINUNSAT16.7310.995.65705103500195474806037
normalized-ooo.tag8.ucl.opbooo32498983FINUNSAT5.244.640.58162222002107187233
normalized-ooo.unbounded.all.ucl.opbooo84836245062FINUNSAT728.8644.63684.035742572200263387411624524
normalized-pigeon-cardinality-101-100.opbpig-card10100201TOUNKT4.69T1000003020090201
normalized-pigeon-cardinality-105-100.opbpig-card10500205TOUNKT4.96T1000003140093805
normalized-pigeon-cardinality-11-10.opbpig-card11021FINUNSAT1.360.231.1110000320921
normalized-pigeon-cardinality-15-10.opbpig-card15025FINUNSAT1.160.420.72100004401285
normalized-pigeon-cardinality-21-20.opbpig-card42041TOUNKT1.56T2000012403641
normalized-pigeon-cardinality-25-20.opbpig-card50045TOUNKT1.17T2000014804365
normalized-pigeon-cardinality-31-30.opbpig-card93061TOUNKT2.56T3000027608161
normalized-pigeon-cardinality-35-30.opbpig-card105065TOUNKT1.58T3000031209245
normalized-pigeon-cardinality-41-40.opbpig-card164081TOUNKT2.62T40000488014481
normalized-pigeon-cardinality-45-40.opbpig-card180085TOUNKT2.97T40000536015925
normalized-pigeon-cardinality-51-50.opbpig-card2550101TOUNKT1.90T50000760022601
normalized-pigeon-cardinality-55-50.opbpig-card2750105TOUNKT1.90T50000820024405
normalized-pigeon-cardinality-61-60.opbpig-card3660121TOUNKT2.35T600001092032521
normalized-pigeon-cardinality-65-60.opbpig-card3900125TOUNKT2.40T600001164034685
normalized-pigeon-cardinality-71-70.opbpig-card4970141TOUNKT3.97T700001484044241
normalized-pigeon-cardinality-75-70.opbpig-card5250145TOUNKT3.87T700001568046765
normalized-pigeon-cardinality-81-80.opbpig-card6480161TOUNKT4.98T800001936057761
normalized-pigeon-cardinality-85-80.opbpig-card6800165TOUNKT4.51T800002032060645
normalized-pigeon-cardinality-91-90.opbpig-card8190181TOUNKT5.24T900002448073081
normalized-pigeon-cardinality-95-90.opbpig-card8550185TOUNKT5.12T900002556076325
normalized-pigeon-clauses-101-100.opbpig-cl10100505101TOUNKT14.43T000010100505101
normalized-pigeon-clauses-105-100.opbpig-cl10500546105TOUNKT17.20T000010500546105
normalized-pigeon-clauses-11-10.opbpig-cl110561FINUNSAT66.260.4665.780000110561
normalized-pigeon-clauses-15-10.opbpig-cl1501065FINUNSAT197.021.41195.6000001501065
normalized-pigeon-clauses-21-20.opbpig-cl4204221TOUNKT3.03T00004204221
normalized-pigeon-clauses-25-20.opbpig-cl5006025TOUNKT3.15T00005006025
normalized-pigeon-clauses-31-30.opbpig-cl93013981TOUNKT3.06T000093013981
normalized-pigeon-clauses-35-30.opbpig-cl105017885TOUNKT3.33T0000105017885
normalized-pigeon-clauses-41-40.opbpig-cl164032841TOUNKT4.88T0000164032841
normalized-pigeon-clauses-45-40.opbpig-cl180039645TOUNKT4.86T0000180039645
normalized-pigeon-clauses-51-50.opbpig-cl255063801TOUNKT4.42T0000255063801
normalized-pigeon-clauses-55-50.opbpig-cl275074305TOUNKT4.65T0000275074305
normalized-pigeon-clauses-61-60.opbpig-cl3660109861TOUNKT5.58T00003660109861
normalized-pigeon-clauses-65-60.opbpig-cl3900124865TOUNKT5.66T00003900124865
normalized-pigeon-clauses-71-70.opbpig-cl4970174021TOUNKT8.25T00004970174021
normalized-pigeon-clauses-75-70.opbpig-cl5250194325TOUNKT8.72T00005250194325
normalized-pigeon-clauses-81-80.opbpig-cl6480259281TOUNKT10.38T00006480259281
normalized-pigeon-clauses-85-80.opbpig-cl6800285685TOUNKT11.29T00006800285685
normalized-pigeon-clauses-91-90.opbpig-cl8190368641TOUNKT13.28T00008190368641
normalized-pigeon-clauses-95-90.opbpig-cl8550401945TOUNKT14.14T00008550401945
normalized-ppp1-11-19-21.opbppp460230179TOUNKT7.35T101900030427145640
normalized-ppp1-12-16.opbppp466231725FINSAT8.027.110.87102900030831148626
normalized-ppp1-13.opbppp463230964FINSAT7.806.820.94102400031028149134
normalized-ppp1-3-13-19.opbppp460830348FINSAT8.887.281.58102000030714147180
normalized-ppp1-9-16-19.opbppp462630747TOUNKT6.81T102300029697142374
normalized-ppp3-13-25-26.opbppp464431254FINSAT16.127.278.81102600031092149640
normalized-robin10.opbrobin2025410FINSAT6.285.310.9523009029894126701
normalized-robin12.opbrobin4356600FINSAT20.634.6215.99336010064662274650
normalized-robin14.opbrobin8281826TOUNKT7.92T4620120123257524180
normalized-robin16.opbrobin144001088TOUNKT11.26T6080140214730913916
normalized-robin18.opbrobin234091386TOUNKT16.77T77401803494831488240
normalized-robin8.opbrobin784256FINSAT2.241.910.311440701146548392
normalized-t2001.13queen13.1110966483.opb13queen169101FINUNSAT3.041.401.6265200575126864
normalized-t2001.13queen13.1110966688.opb13queen169101FINUNSAT4.871.593.2665200594827849
normalized-t2001.13queen13.1110967142.opb13queen169101FINUNSAT8.581.337.2465200621229169
normalized-t2001.13queen13.1110967327.opb13queen169101FINSAT4.211.432.7665200620029109
normalized-t2001.13queen13.1110967523.opb13queen169101FINUNSAT6.211.384.8165200613928804
normalized-t2001.13queen13.1110967729.opb13queen169101FINUNSAT3.281.401.8665200563426279
normalized-t2001.13queen13.1110968094.opb13queen169101FINUNSAT5.401.653.7365200596127914
normalized-t2001.13queen13.1110968431.opb13queen169101FINSAT2.391.500.8765200588327524
normalized-t2001.13queen13.1110968561.opb13queen169101FINUNSAT6.491.425.0565200595127864
normalized-t2001.13queen13.1110968898.opb13queen169101FINUNSAT6.431.654.7665200592727744
normalized-t2001.13queen13.1110969170.opb13queen169101FINUNSAT5.011.393.6065200611228669
normalized-t2001.13queen13.1110969577.opb13queen169101FINUNSAT4.411.502.8965200596127914
normalized-t2001.13queen13.1110969860.opb13queen169101FINUNSAT8.041.616.4165200632029709
normalized-t2001.13queen13.1110969933.opb13queen169101FINSAT3.151.431.7065200589027559
normalized-t2001.13queen13.1110970170.opb13queen169101FINSAT4.201.422.7665200614128814
normalized-t2001.13queen13.1110970277.opb13queen169101FINSAT3.471.481.9765200626629439
normalized-t2001.13queen13.1110970444.opb13queen169101FINUNSAT3.561.432.1165200604728344
normalized-t2001.13queen13.1110970631.opb13queen169101FINUNSAT3.811.492.3065200571226669
normalized-t2001.13queen13.1110971097.opb13queen169101FINSAT5.691.544.1365200628229519
normalized-t2001.13queen13.1110971363.opb13queen169101FINUNSAT4.601.662.9265200610328624
normalized-t2001.13queen13.1110971697.opb13queen169101FINUNSAT5.351.693.6465200600728144
normalized-t2001.13queen13.1110971766.opb13queen169101FINSAT3.052.260.7765200597027959
normalized-t2001.13queen13.1110972154.opb13queen169101FINUNSAT5.931.544.3665200604128314
normalized-t2001.13queen13.1110972763.opb13queen169101FINUNSAT5.401.364.0265200607428479
normalized-t2001.13queen13.1110972958.opb13queen169101FINSAT2.011.380.6165200616828949
normalized-t2001.13queen13.1110973163.opb13queen169101FINUNSAT8.061.466.5865200612828749
normalized-t2001.13queen13.1110973364.opb13queen169101FINUNSAT4.151.352.7865200597727994
normalized-t2001.13queen13.1110973478.opb13queen169101FINSAT4.731.423.2965200609328574
normalized-t2001.13queen13.1110973670.opb13queen169101FINUNSAT5.711.424.2765200591927704
normalized-t2001.13queen13.1110973863.opb13queen169101FINSAT7.751.736.0065200603828299
normalized-t2001.13queen13.1110974180.opb13queen169101FINUNSAT6.952.254.6765200600328124
normalized-t2001.13queen13.1110974372.opb13queen169101FINUNSAT3.831.482.3365200598328024
normalized-t2001.13queen13.1110974553.opb13queen169101FINSAT4.002.331.6565200620829149
normalized-t2001.13queen13.1110975607.opb13queen169101FINUNSAT3.411.342.0565200601928204
normalized-t2001.13queen13.1110975678.opb13queen169101FINSAT3.201.331.8565200609828599
normalized-t2001.13queen13.1110975832.opb13queen169101FINSAT4.791.503.2765200625029359
normalized-t2001.13queen13.1110975965.opb13queen169101FINUNSAT9.501.458.0365200625829399
normalized-t2001.13queen13.1110976157.opb13queen169101FINUNSAT3.461.471.9765200583427279
normalized-t2001.13queen13.1110976730.opb13queen169101FINUNSAT9.291.497.7865200618629039
normalized-t2001.13queen13.1110976735.opb13queen169101FINSAT3.381.681.6865200634029809
normalized-t2001.13queen13.1110976935.opb13queen169101FINUNSAT3.921.292.6165200600828149
normalized-t2001.13queen13.1110977266.opb13queen169101FINSAT4.361.662.6865200603528284
normalized-t2001.13queen13.1110977273.opb13queen169101FINUNSAT5.611.344.2565200598428029
normalized-t2001.13queen13.1110977464.opb13queen169101FINSAT8.651.646.9965200610428629
normalized-t2001.13queen13.1110977780.opb13queen169101FINUNSAT3.991.492.4865200576326924
normalized-t2001.13queen13.1110978113.opb13queen169101FINUNSAT7.581.456.1165200612128714
normalized-t2001.13queen13.1110978334.opb13queen169101FINUNSAT5.162.322.8265200601728194
normalized-t2001.13queen13.1111212272.opb13queen169101FINUNSAT6.201.454.7365200609628589
normalized-t2001.13queen13.1111212476.opb13queen169101FINUNSAT7.321.425.8865200630929654
normalized-t2001.13queen13.1111212923.opb13queen169101FINUNSAT4.921.563.3465200600428129
normalized-t2001.13queen13.1111213670.opb13queen169101FINUNSAT4.821.693.1165200613028759
normalized-t2001.13queen13.1111213868.opb13queen169101FINUNSAT5.381.613.7465200621129164
normalized-t2001.13queen13.1111216188.opb13queen169101FINSAT2.761.461.2865200607128464
normalized-t2001.13queen13.1111216411.opb13queen169101FINUNSAT6.161.494.6565200603228269
normalized-t2001.13queen13.1111216823.opb13queen169101FINUNSAT5.321.563.7465200606728444
normalized-t2001.13queen13.1111216864.opb13queen169101FINSAT4.071.602.4565200604728344
normalized-t2001.13queen13.1111217374.opb13queen169101FINSAT1.981.590.3765200633629789
normalized-t2001.13queen13.1111217380.opb13queen169101FINSAT2.391.670.7065200614728844
normalized-t2001.13queen13.1111217392.opb13queen169101FINUNSAT4.541.503.0265200594927854
normalized-t2001.13queen13.1111217555.opb13queen169101FINUNSAT6.442.094.3365200599828099
normalized-t2001.13queen13.1111218024.opb13queen169101FINUNSAT5.271.533.7265200603228269
normalized-t2001.13queen13.1111218308.opb13queen169101FINUNSAT12.001.6010.3765200623929304
normalized-t2001.13queen13.1111218757.opb13queen169101FINUNSAT6.361.694.6565200596927954
normalized-t2001.13queen13.1111218955.opb13queen169101FINUNSAT4.121.442.6665200612228719
normalized-t2001.13queen13.1111219348.opb13queen169101FINUNSAT5.111.763.3365200608328524
normalized-t2001.13queen13.1111219399.opb13queen169101FINSAT2.131.450.6765200605928404
normalized-t2001.13queen13.1111219799.opb13queen169101FINUNSAT4.041.462.5565200593827799
normalized-t2001.13queen13.1111220019.opb13queen169101FINUNSAT4.821.523.2865200588327524
normalized-t2001.13queen13.1111220546.opb13queen169101FINUNSAT5.491.663.8165200592827749
normalized-t2001.13queen13.1111220767.opb13queen169101FINUNSAT6.121.644.4665200599128064
normalized-t2001.13queen13.1111221203.opb13queen169101FINUNSAT5.451.254.1865200597327974
normalized-t2001.13queen13.1111221624.opb13queen169101FINUNSAT5.561.673.8665200602728244
normalized-t2001.13queen13.1111221953.opb13queen169101FINSAT2.881.441.4265200587527484
normalized-t2001.13queen13.1111222080.opb13queen169101FINSAT5.701.554.1365200601228169
normalized-t2001.13queen13.1111222248.opb13queen169101FINSAT3.241.451.7765200631129664
normalized-t2001.13queen13.1111222257.opb13queen169101FINUNSAT4.841.553.2865200598928054
normalized-t2001.13queen13.1111222539.opb13queen169101FINUNSAT6.351.514.8265200621629189
normalized-t2001.13queen13.1111223004.opb13queen169101FINUNSAT7.021.455.5565200597527984
normalized-t2001.13queen13.1111223220.opb13queen169101FINUNSAT5.991.604.3765200604028309
normalized-t2001.13queen13.1111223416.opb13queen169101FINSAT2.902.300.5865200604228319
normalized-t2001.13queen13.1111223596.opb13queen169101FINSAT4.241.452.7665200596127914
normalized-t2001.13queen13.1111223689.opb13queen169101FINSAT1.741.520.2065200621529184
normalized-t2001.13queen13.1111223696.opb13queen169101FINSAT2.551.640.8965200591827699
normalized-t2001.13queen13.1111224059.opb13queen169101FINUNSAT3.831.662.1565200575026859
normalized-t2001.13queen13.1111224255.opb13queen169101FINUNSAT5.691.664.0165200605228369
normalized-t2001.13queen13.1111224451.opb13queen169101FINUNSAT5.101.593.4965200593927804
normalized-t2001.13queen13.1111224522.opb13queen169101FINSAT2.841.711.1165200585127364
normalized-t2001.13queen13.1111224929.opb13queen169101FINUNSAT3.981.462.4965200588927554
normalized-t2001.13queen13.1111225122.opb13queen169101FINUNSAT3.791.652.1265200593927804
normalized-t2001.13queen13.1111225605.opb13queen169101FINUNSAT4.541.413.1165200600528134
normalized-t2001.13queen13.1111226062.opb13queen169101FINUNSAT4.511.642.8565200595727894
normalized-t2001.13queen13.1111226241.opb13queen169101FINSAT2.481.500.9765200620929154
normalized-t2001.13queen13.1111226284.opb13queen169101FINSAT4.761.683.0665200612828749
normalized-t2001.13queen13.1111226368.opb13queen169101FINUNSAT4.561.652.8965200586327424
normalized-t2001.13queen13.1111226680.opb13queen169101FINUNSAT6.521.514.9965200617828999
normalized-t2001.13queen13.1111227012.opb13queen169101FINUNSAT5.931.734.1865200603028259
normalized-t2001.13queen13.1111227326.opb13queen169101FINUNSAT3.571.661.8965200591827699
normalized-t2001.13queen13.1111227418.opb13queen169101FINSAT3.941.612.3165200611828699
normalized-t2001.13queen13.1111227861.opb13queen169101FINUNSAT4.811.663.1365200591727694
normalized-t2001.13queen13.1111228076.opb13queen169101FINUNSAT7.901.766.1265200602128214
normalized-t3002.11tsp11.1900544463.opb11tsp112312707FINSAT4.373.630.7223000265014310
normalized-t3002.11tsp11.1900544484.opb11tsp112312707FINUNSAT19.293.8115.4623000241813150
normalized-t3002.11tsp11.1900545610.opb11tsp112312707FINUNSAT36.974.0632.8923000265814350
normalized-t3002.11tsp11.1900546076.opb11tsp112312707FINUNSAT4.804.170.6123000254213770
normalized-t3002.11tsp11.1900546417.opb11tsp112312707FINUNSAT26.134.0222.0923000253813750
normalized-t3002.11tsp11.1900547334.opb11tsp112312707FINSAT4.413.910.4823000262214170
normalized-t3002.11tsp11.1900547353.opb11tsp112312707FINSAT4.223.900.3023000241413130
normalized-t3002.11tsp11.1900547389.opb11tsp112312707FINUNSAT33.243.9829.2323000255213820
normalized-t3002.11tsp11.1900547416.opb11tsp112312707FINSAT2.472.110.3423000242413180
normalized-t3002.11tsp11.1900547427.opb11tsp112312707FINSAT4.634.070.5423000266014360
normalized-t3002.11tsp11.1900547461.opb11tsp112312707FINSAT4.163.760.3823000256813900
normalized-t3002.11tsp11.1900548667.opb11tsp112312707FINUNSAT90.323.6986.6123000275214820
normalized-t3002.11tsp11.1900549974.opb11tsp112312707FINSAT4.563.720.8223000263414230
normalized-t3002.11tsp11.1900550006.opb11tsp112312707FINUNSAT55.652.8652.7723000262814200
normalized-t3002.11tsp11.1900550720.opb11tsp112312707FINUNSAT46.553.5642.9723000260414080
normalized-t3002.11tsp11.1900551347.opb11tsp112312707FINUNSAT5.583.771.7923000245613340
normalized-t3002.11tsp11.1900551864.opb11tsp112312707FINUNSAT9.413.935.4623000254813800
normalized-t3002.11tsp11.1900552288.opb11tsp112312707FINUNSAT27.093.6423.4323000250613590
normalized-t3002.11tsp11.1900552311.opb11tsp112312707FINSAT3.032.800.2123000245213320
normalized-t3002.11tsp11.1900552423.opb11tsp112312707FINUNSAT5.014.210.7823000234212770
normalized-t3002.11tsp11.1900552735.opb11tsp112312707FINUNSAT5.013.801.1923000250813600
normalized-t3002.11tsp11.1900553606.opb11tsp112312707FINSAT3.592.301.2723000264414280
normalized-t3002.11tsp11.1900553644.opb11tsp112312707FINSAT4.053.860.1723000265814350
normalized-t3002.11tsp11.1900553647.opb11tsp112312707FINUNSAT39.993.7636.2123000252613690
normalized-t3002.11tsp11.1900553812.opb11tsp112312707FINUNSAT4.883.890.9723000254013760
normalized-t3002.11tsp11.1900554067.opb11tsp112312707FINSAT4.564.000.5423000279015010
normalized-t3002.11tsp11.1900554072.opb11tsp112312707FINUNSAT24.143.7320.3923000258613990
normalized-t3002.11tsp11.1900554154.opb11tsp112312707FINSAT4.013.830.1623000267614440
normalized-t3002.11tsp11.1900554373.opb11tsp112312707FINSAT4.123.920.1823000280015060
normalized-t3002.11tsp11.1900554375.opb11tsp112312707FINSAT4.384.170.1923000266814400
normalized-t3002.11tsp11.1900554389.opb11tsp112312707FINSAT4.233.820.3823000261014110
normalized-t3002.11tsp11.1900554420.opb11tsp112312707FINUNSAT7.463.883.5623000259814050
normalized-t3002.11tsp11.1900556231.opb11tsp112312707FINUNSAT22.243.9018.3223000247013410
normalized-t3002.11tsp11.1900557362.opb11tsp112312707FINUNSAT3.132.230.8723000259214020
normalized-t3002.11tsp11.1900557413.opb11tsp112312707FINSAT4.583.840.7123000277214920
normalized-t3002.11tsp11.1900557568.opb11tsp112312707FINSAT3.883.710.1523000280415080
normalized-t3002.11tsp11.1900557574.opb11tsp112312707FINUNSAT11.164.586.5523000256013860
normalized-t3002.11tsp11.1900557957.opb11tsp112312707FINUNSAT20.202.4417.7323000253613740
normalized-t3002.11tsp11.1900558106.opb11tsp112312707FINUNSAT4.694.360.3123000227412430
normalized-t3002.11tsp11.1900558739.opb11tsp112312707FINUNSAT35.353.8231.5023000266214370
normalized-t3002.11tsp11.1900559365.opb11tsp112312707FINSAT4.493.950.5123000256213870
normalized-t3002.11tsp11.1900559416.opb11tsp112312707FINSAT5.963.852.0923000266814400
normalized-t3002.11tsp11.1900559641.opb11tsp112312707FINSAT4.974.650.3023000261714145
normalized-t3002.11tsp11.1900559676.opb11tsp112312707FINUNSAT68.584.2964.2723000276214870
normalized-t3002.11tsp11.1900561288.opb11tsp112312707FINUNSAT94.032.2591.7623000277014910
normalized-t3002.11tsp11.1900561384.opb11tsp112312707FINSAT4.083.810.2523000288015460
normalized-t3002.11tsp11.1900561389.opb11tsp112312707FINSAT4.553.700.8323000249813550
normalized-t3002.11tsp11.1900562192.opb11tsp112312707FINUNSAT8.182.275.8923000239413030
normalized-t3002.11tsp11.1900563250.opb11tsp112312707FINUNSAT24.092.3221.7523000262214170
normalized-t3002.11tsp11.1900563801.opb11tsp112312707FINUNSAT6.003.572.4123000249213520
normalized-t3002.11tsp11.1900564281.opb11tsp112312707FINUNSAT5.583.931.6323000260414080
normalized-t3002.11tsp11.1900564822.opb11tsp112312707FINSAT3.913.690.2023000273414730
normalized-t3002.11tsp11.1900564824.opb11tsp112312707FINUNSAT4.363.580.7623000225412330
normalized-t3002.11tsp11.1900565527.opb11tsp112312707FINSAT4.133.680.4323000247813450
normalized-t3002.11tsp11.1900565534.opb11tsp112312707FINUNSAT21.123.7717.3323000259414030
normalized-t3002.11tsp11.1900566151.opb11tsp112312707FINSAT4.704.460.2223000261614140
normalized-t3002.11tsp11.1900566157.opb11tsp112312707FINUNSAT13.883.4410.4223000228212470
normalized-t3002.11tsp11.1900566263.opb11tsp112312707FINSAT3.983.770.1923000277614940
normalized-t3002.11tsp11.1900566270.opb11tsp112312707FINSAT4.063.810.2323000283015210
normalized-t3002.11tsp11.1900567003.opb11tsp112312707FINSAT4.774.330.4223000249813550
normalized-t3002.11tsp11.1900567024.opb11tsp112312707FINUNSAT4.012.201.7923000239413030
normalized-t3002.11tsp11.1900567135.opb11tsp112312707FINUNSAT14.653.6510.9823000241613140
normalized-t3002.11tsp11.1900567939.opb11tsp112312707FINSAT3.823.640.1623000257613940
normalized-t3002.11tsp11.1900567985.opb11tsp112312707FINUNSAT29.883.7426.1223000263414230
normalized-t3002.11tsp11.1900568186.opb11tsp112312707FINUNSAT6.663.892.7523000252413680
normalized-t3002.11tsp11.1900568706.opb11tsp112312707FINUNSAT17.993.9214.0523000258013960
normalized-t3002.11tsp11.1900568952.opb11tsp112312707FINSAT4.033.670.3423000262414180
normalized-t3002.11tsp11.1900569834.opb11tsp112312707FINUNSAT11.723.668.0423000251813652
normalized-t3002.11tsp11.1900570242.opb11tsp112312707FINUNSAT7.613.743.8523000247413430
normalized-t3002.11tsp11.1900571131.opb11tsp112312707FINSAT4.123.750.3523000264814300
normalized-t3002.11tsp11.1900571132.opb11tsp112312707FINUNSAT46.043.8042.2223000239013010
normalized-t3002.11tsp11.1900571761.opb11tsp112312707FINUNSAT40.073.7336.3123000252613690
normalized-t3002.11tsp11.1900573137.opb11tsp112312707FINUNSAT27.442.2225.2023000258213970
normalized-t3002.11tsp11.1900573901.opb11tsp112312707FINUNSAT39.623.7635.8423000254813800
normalized-t3002.11tsp11.1900574864.opb11tsp112312707FINUNSAT11.383.517.8423000262214170
normalized-t3002.11tsp11.1900574948.opb11tsp112312707FINSAT4.664.380.2623000259214020
normalized-t3002.11tsp11.1900574974.opb11tsp112312707FINSAT3.823.620.1823000260214070
normalized-t3002.11tsp11.1900575442.opb11tsp112312707FINUNSAT20.333.6816.6323000260014060
normalized-t3002.11tsp11.1900576151.opb11tsp112312707FINUNSAT45.592.2143.3623000255213820
normalized-t3002.11tsp11.1900576360.opb11tsp112312707FINUNSAT19.173.7215.4323000246613390
normalized-t3002.11tsp11.1900576918.opb11tsp112312707FINSAT4.123.720.3823000270814600
normalized-t3002.11tsp11.1900576927.opb11tsp112312707FINUNSAT47.333.6743.6423000262214170
normalized-t3002.11tsp11.1900577000.opb11tsp112312707FINSAT2.462.230.2123000270214570
normalized-t3002.11tsp11.1900577940.opb11tsp112312707FINUNSAT63.693.7859.8923000260814100
normalized-t3002.11tsp11.1900579996.opb11tsp112312707FINUNSAT65.003.8061.1823000255913855
normalized-t3002.11tsp11.1900581320.opb11tsp112312707FINUNSAT48.803.6345.1523000268814500
normalized-t3002.11tsp11.1900581321.opb11tsp112312707FINSAT4.254.040.1923000268414480
normalized-t3002.11tsp11.1900582300.opb11tsp112312707FINUNSAT64.443.8560.5723000265014310
normalized-t3002.11tsp11.1900582376.opb11tsp112312707FINSAT3.923.630.2723000242013160
normalized-t3002.11tsp11.1900583053.opb11tsp112312707FINUNSAT58.093.4954.5823000267614440
normalized-t3002.11tsp11.1900584106.opb11tsp112312707FINUNSAT3.982.201.7623000253413730
normalized-t3002.11tsp11.1900584219.opb11tsp112312707FINUNSAT12.553.738.8023000261214120
normalized-t3002.11tsp11.1900667195.opb11tsp112312707FINUNSAT46.503.7842.7023000267014410
normalized-t3002.11tsp11.1900669299.opb11tsp112312707FINSAT2.472.110.3423000253413730
normalized-t3002.11tsp11.1900669309.opb11tsp112312707FINSAT3.942.281.6423000266814400
normalized-t3002.11tsp11.1900669797.opb11tsp112312707FINUNSAT34.852.2832.5523000258213970
normalized-t3002.11tsp11.1900670167.opb11tsp112312707FINUNSAT22.892.5520.3223000256613890
normalized-t3002.11tsp11.1900670234.opb11tsp112312707FINUNSAT77.683.6674.0023000273414730
normalized-t3002.11tsp11.1900670675.opb11tsp112312707FINUNSAT8.513.914.5923000261414130
normalized-t3002.11tsp11.1900670756.opb11tsp112312707FINSAT3.953.630.3023000258814000
normalized-vdw_k3_l5_n550.opbvdw1650113164FINSAT376.346.93369.1700001650114814
normalized-vdw_k3_l6_n1500.opbvdw4500674250FINSAT96.8041.7353.7000004500678750
normalized-vdw_k4_l4_n360.opbvdw144086040TOUNKT5.72T360000396096120
normalized-vdw_k5_l4_n750.opbvdw3750467625TOUNKT20.88T75000010500495375
normalized-vdw_k6_l3_n170.opbvdw102043010TOUNKT3.39T170000289050830

References

  • [AbioNORM12] Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Valentin Mayer-Eichberger. A New Look at BDDs for Pseudo-Boolean Constraints. Journal of Artificial Intelligence Research, 45:443-480, 2012.
  • [EenS06] Niklas Eén and Niklas Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006.
  • [BailleuxBR09] Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of pseudo-Boolean constraints into CNF. In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), LNCS 5584, pages 181-194, 2009.
  • [ManquinhoS06] Vasco M. Manquinho and João P. Marques Silva. On using cutting planes in pseudo-Boolean optimization. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):209-219, 2006.
  • [BerreP10] Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):59-6, 2010.
  • [ManquinhoML10] Vasco M. Manquinho, Ruben Martins, and Inês Lynce. Improving unsatisfiability-based algorithms for Boolean optimization. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), LNCS 6175, pages 181-193, 2010.
  • [SilverthornM10] Bryan Silverthorn and Risto Miikkulainen. Latent class models for algorithm portfolio methods. In Proceedings of the 24th National Conference on Artificial Intelligence (AAAI 2010), 2010.
  • [GebserKNS07] Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub. Conflict-driven answer set solving. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI 2007), AAAI Press/MIT Press, pages 386-392, 2007.

?????

Date: 2020-12-14 12:20:31 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 26

Validate XHTML 1.0