Spying on lingeling
Generated by
SpySMAC (S. Falkner, M. Lindauer and F. Hutter).
- Final Configuration Details
-
cintmaxhard=10000000 cce3wait=2 deco=1 saturating=70 lkhdmisifelmrtc=0 elim=1 move=2 rstinoutinc=135 unhdextstamp=1 simpvarchg=100 minimize=2 bva=0 elmreleff=200 delmax=10 blklarge=1 elmblk=1 liftwait=2 rephaseinc=10000 lftroundlim=1019633314 locsmaxeff=100000 compact=0 prbasicroundlim=236 ternres=1 flipvlim=100000 carduse=2 unhdlnpr=3 cliff=1 cardmaxlen=1000 trnrmineff=4000000 ccemineff=30000000 cardmineff=2000000 synclsint=100 bcawait=2 score=4 blkreleff=100 maxscorexp=500 rdpreleff=2 elmsuccesslim=1000 blkmineff=1930951988 locswait=2 cceonlyifstuck=0 syncunint=439424 unhdhbr=0 probe=1 sortlits=0 psm=3 gluescale=4 redlexpfac=131 randecflipint=97775439 unhdatrn=2 actvlim=169133023 dlim=-1 boost=1 bumpseenlits=1 prbasicmineff=1000000 transred=1 tabrkeep=3 elmocclim=1000000 restart=2 locsred=0 transredwait=2 bumpseenbeforemin=1 cgrmaxority=20 treelookrtc=0 locsclim=4812804 redinoutinc=100 cgrextxor=1 synclslen=40 elmfull=0 blockwait=1 locscint=10000 elmineff=20000000 sizemaxpen=5 simpidiv=3 blksuccesslim=10000 megaint=4 liftlrg=3 synclsall=1 locsvared=100 redfixed=0 blksmall=1 cgrexteq=1 force=0 cce=3 prbsimpleboost=10 bias=2 cgrextunits=1 reduce=1 blkschedmin=0 trdreleff=10 actstdmax=112 gaussextrall=1 cardmaxeff=300000000 cliffwait=2 randec=0 actstdmin=10 cardcut=2 reusetrail=1 unhdmaxeff=615417944 treelook=1 trnreleff=10 cardreleff=5 unhide=1 redoutvlim=1000 batewait=2 actgeomlim=2 locsrtc=0 redloutinc=10000 minrecgluelim=20 phasegluebit=0 tabrcfactor=25 cardreschedint=10 locsdec=2 import=1 redoutclim=5000 prbasic=1 lftmaxeff=20000000 incsavevisits=0 ternresrtc=0 mocint=1000 gaussexptrn=1 elmaxeff=194654227 binsimpdel=2 otfsconf=0 cliffreleff=8 bumpclslits=0 redlminrel=10 subl=9 actdblarithlim=3 redlminabs=500 bumpseenaftermin=0 simpen=0 rephase=1 elmocclim1=1000 smallvewait=0 treelookboost=1 cardocclim2=15 blksuccessrat=41111 prbrtc=0 elmblkwait=1 card=1 simprtc=5 bkwdscale=2 smallve=1 prbsimplemaxeff=200000000 prbasicreleff=10 rdp=0 gaussmaxor=20 simplify=2 cardocclim1=300 redlbound=0 defragfree=113 blkocclim1=100000 defragint=1937183975 elmclslim=1000000 treelookfull=0 redlinc=1000 agile=1 sizepen=11914060 gausswait=2 block=1 locsboost=2 memlim=-1 bate=1 decompose=1 tabrvfactor=4 locsreleff=5 cgrextite=1 elmocclim2=100 cardexpam1=3 flipping=1 termint=122222 elmroundlim=3 cgrmineff=200000 redlmininc=10 redlmaxrel=9740 keepmaxglue=1 otfsbump=0 factor=3 locsmineff=930082428 synclsglue=8 rdpwait=2 cceboost=10 trdmineff=100000 blkschedprod=0 cgrclsr=1 itsimpdel=20 cliffmineff=10000000 gaussreleff=2 trepint=55555 cgreleff=1 unhidewait=0 itlocsdel=100 elmsched2b2=0 treelooklrg=1 treelookmaxeff=1237851481 prbsimpleliftdepth=2 wait=1 locset=2 cardglue=0 blkmaxeff=666095051 simpiscale=100 elmsuccessrat=1000 incredconfslim=0 prbsimple=2 lhbr=1 phaseflip=0 unhdreleff=2 bcaminuse=100 trnrmaxeff=13279633 blkrtc=0 prbasicmaxeff=100000000 gauss=1 unhdroundlim=43 otfs=1 lift=1 cce2wait=1 locsexport=1 prbsimplemineff=750031617 unhdmineff=345815310 mega=0 seed=0 actgsdul=7 agilesinint=3007633 megawait=2 rmincpen=4 ccewait=2 elmboost=40 restartint=5 simpdelay=0 plain=0 redlmaxinc=31 restartinit=0 elmschedsum=1 irrlim=1 elmschedmin=0 fliptop=1 treelookmineff=300000 prbsimplereleff=4634 binlocsdel=10 bcamaxeff=10000000 trep=0 blkboostvlim=1000000 ccereleff=137 lftreleff=6 cgrclsrwait=2 elmschedpure=1 rdpmaxeff=10000000 maxglue=2147483647 redlmaxabs=1000000 elmschedprod=0 factmax=100000 tabr=1 bumpseenminsize=3 incredcint=1 smallirr=90 cgrextand=1 cceboostvlim=1000000 locs=309517807 rdpmineff=10000 blksched2b2=0 ccemaxeff=2147483647 cliffmaxeff=100000000 actavgmax=112 blkocclim2=10000 cardwait=0 clim=-1 blkschedpure=1 cintmaxsoft=438400341 cintinc=20000 prbasicrtc=0 lftmineff=500000 smallvevars=10 blkschedsum=1 bumpbcplits=0 acts=2 fliplevels=6 blkboost=2539 penmax=4 ccesuccessrat=1000 scincinc=200 rdpclslim=444808145 pure=0 ternreswait=2 cgrmaxeff=8000000 ternresboost=5 rdpmodelm=0 flipdur=10 cintincdiv=2 gaussmaxeff=50000000 prbsimplertc=0 waitmax=4 randecint=17790 elmlitslim=200 inprocessing=1 minlocalgluelim=30 phaseneginit=0 redlinit=4000 jwhred=1 lkhd=1 treelookreleff=1 ccertc=0 ccesuccesslim=10000 cardignused=0 agilelim=30 phase=0 simpinterdelay=2000 blkclslim=1000000 simpvarlim=100 plim=-1 cardminlen=181074193 flipldmod=4 flipint=10 gaussmineff=2000000 gluekeep=3 blkocclim=1000000 decolim=30 bca=1 elmrtc=0 rdplim=100 restartintscale=0 trdmaxeff=2000000 elmschediff=0
- Meta Data Details
-
Solver | lingeling |
#Instances (Test) | 351 |
#Instances (Train) | 1032 |
os system | Linux |
os release | 3.13.0-39-generic |
cpu vendor | GenuineIntel |
cpu brand | Intel(R) Xeon(R) CPU E5-2650 v2 @ 2.60GHz |
cpu hz | 2.6000 GHz |
cpu arch | X86_64 |
cpu count | 16 |
cutoff | 300 |
verbosity | INFO |
repetitions | 1 |
budget | 86400 |
prefix | - |
seed | 0 |
memory | 2000 |
outputdir | . |
- Performance Overview Details
-
Test Performance
| Default | Configured |
Average Runtime | 27.49 | 19.81 |
PAR10 | 112.10 | 58.28 |
Timeouts | 11 / 351 | 5 / 351 |
Training Performance
| Default | Configured |
Average Runtime | 28.09 | 21.89 |
PAR10 | 140.59 | 84.68 |
Timeouts | 43 / 1032 | 24 / 1032 |
- Scatter Plot Details
-
- CDF Plot Details
-
- Cactus Plot Details
-
- Parameter Importance over Default Details
-
Parameter | Importance |
blkboostvlim | 3.48 |
decolim | 2.53 |
simpdelay | 2.22 |
minlocalgluelim | 2.09 |
redlinit | 1.71 |
gaussmaxeff | 1.66 |
flipdur | 1.58 |
treelookmaxeff | 1.46 |
scincinc | 1.37 |
termint | 1.24 |
- Parameter Importance over Default Plots Details
- Parameter Importance over Nothing Details
-
Parameter | Importance |
score | 9.85 |
subl | 2.91 |
gluekeep | 0.85 |
cliffmaxeff | 0.68 |
dlim | 0.36 |
saturating | 0.32 |
trepint | 0.32 |
blkboost | 0.30 |
synclslen | 0.27 |
cardmaxlen | 0.25 |
- Parameter Importance over Nothing Plots Details