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=110 unhdextstamp=1 simpvarchg=100 minimize=2 bva=0 elmreleff=200 delmax=10 blklarge=1 elmblk=1 liftwait=2 rephaseinc=10000 lftroundlim=5 locsmaxeff=100000 compact=0 prbasicroundlim=9 ternres=1 flipvlim=100000 carduse=2 unhdlnpr=3 cliff=1 cardmaxlen=1000 trnrmineff=1016610578 ccemineff=30000000 cardmineff=2000000 synclsint=100 bcawait=2 score=5 blkreleff=100 maxscorexp=500 rdpreleff=2 elmsuccesslim=1000 blkmineff=50000000 locswait=2 cceonlyifstuck=0 syncunint=111111 unhdhbr=0 probe=1 sortlits=0 psm=3 gluescale=4 redlexpfac=10 randecflipint=0 unhdatrn=2 actvlim=200000 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=1000000 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=2 blkschedmin=0 trdreleff=1305 actstdmax=112 gaussextrall=1 cardmaxeff=300000000 cliffwait=2 randec=0 actstdmin=10 cardcut=2 reusetrail=1 unhdmaxeff=20000000 treelook=1 trnreleff=10 cardreleff=5 unhide=1 redoutvlim=1000 batewait=2 actgeomlim=1 locsrtc=0 redloutinc=10000 minrecgluelim=20 phasegluebit=0 tabrcfactor=2 cardreschedint=10 locsdec=0 import=1 redoutclim=84451436 prbasic=1 lftmaxeff=55245734 incsavevisits=0 ternresrtc=0 mocint=5946 gaussexptrn=1 elmaxeff=800000000 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=20 cardocclim2=15 blksuccessrat=1000 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=50 blkocclim1=100000 defragint=10000000 elmclslim=1000000 treelookfull=0 redlinc=1000 agile=1 sizepen=1000000 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=300 keepmaxglue=1 otfsbump=0 factor=2 locsmineff=1000 synclsglue=8 rdpwait=2 cceboost=10 trdmineff=100000 blkschedprod=0 cgrclsr=1 itsimpdel=20 cliffmineff=10000000 gaussreleff=2 trepint=783195 cgreleff=1 unhidewait=0 itlocsdel=100 elmsched2b2=0 treelooklrg=1 treelookmaxeff=50000000 prbsimpleliftdepth=2 wait=1 locset=2 cardglue=0 blkmaxeff=800000000 simpiscale=5 elmsuccessrat=1000 incredconfslim=0 prbsimple=2 lhbr=0 phaseflip=0 unhdreleff=944 bcaminuse=100 trnrmaxeff=200000000 blkrtc=0 prbasicmaxeff=100000000 gauss=1 unhdroundlim=20 otfs=1 lift=1 cce2wait=1 locsexport=1 prbsimplemineff=2000000 unhdmineff=633894531 mega=0 seed=0 actgsdul=7 agilesinint=100000 megawait=2 rmincpen=4 ccewait=2 elmboost=40 restartint=5 simpdelay=0 plain=0 redlmaxinc=200 restartinit=0 elmschedsum=1 irrlim=1 elmschedmin=1 fliptop=1 treelookmineff=300000 prbsimplereleff=40 binlocsdel=10 bcamaxeff=10000000 trep=0 blkboostvlim=1000000 ccereleff=20 lftreleff=6 cgrclsrwait=2 elmschedpure=1 rdpmaxeff=10000000 maxglue=2147483647 redlmaxabs=1000000 elmschedprod=0 factmax=2951 tabr=3 bumpseenminsize=3 incredcint=1 smallirr=90 cgrextand=1 cceboostvlim=1000000 locs=0 rdpmineff=10000 blksched2b2=0 ccemaxeff=2147483647 cliffmaxeff=100000000 actavgmax=112 blkocclim2=10000 cardwait=0 clim=-1 blkschedpure=1 cintmaxsoft=1000000 cintinc=159260 prbasicrtc=0 lftmineff=500000 smallvevars=10 blkschedsum=1 bumpbcplits=0 acts=2 fliplevels=6 blkboost=10 penmax=4 ccesuccessrat=8 scincinc=200 rdpclslim=3 pure=1 ternreswait=2 cgrmaxeff=1000402474 ternresboost=5 rdpmodelm=0 flipdur=10 cintincdiv=1 gaussmaxeff=50000000 prbsimplertc=0 waitmax=4 randecint=1000 elmlitslim=200 inprocessing=1 minlocalgluelim=30 phaseneginit=0 redlinit=4000 jwhred=1 lkhd=2 treelookreleff=1 ccertc=0 ccesuccesslim=10000 cardignused=0 agilelim=30 phase=0 simpinterdelay=2000 blkclslim=1000000 simpvarlim=100 plim=-1 cardminlen=3 flipldmod=4 flipint=765139667 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) | 302 |
#Instances (Train) | 299 |
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 | 47.79 | 44.24 |
PAR10 | 316.00 | 276.69 |
Timeouts | 30 / 302 | 26 / 302 |
Training Performance
| Default | Configured |
Average Runtime | 40.43 | 36.79 |
PAR10 | 248.13 | 199.33 |
Timeouts | 23 / 299 | 18 / 299 |
- Scatter Plot Details
-
- CDF Plot Details
-
- Cactus Plot Details
-
- Parameter Importance over Default Details
-
Parameter | Importance |
decolim | 21.53 |
randecflipint | 5.78 |
blksuccessrat | 3.70 |
rstinoutinc | 3.38 |
cgrmineff | 3.26 |
actvlim | 2.94 |
restartinit | 2.83 |
synclslen | 2.58 |
cgreleff | 2.52 |
redoutvlim | 2.24 |
- Parameter Importance over Default Plots Details
- Parameter Importance over Nothing Details
-
Parameter | Importance |
score | 24.95 |
minlocalgluelim | 6.52 |
blkclslim | 0.85 |
gaussreleff | 0.85 |
blksuccesslim | 0.79 |
seed | 0.70 |
unhdlnpr | 0.51 |
gluekeep | 0.47 |
trnrmaxeff | 0.47 |
blkboostvlim | 0.47 |
- Parameter Importance over Nothing Plots Details