probSAT CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/probSAT/probSATWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -luby '1' -cb1 '3.183526684103694' -fct '0' -randomc '1' -eps '1.2156962826935067' -xor '1' -caching '1' -base '103924' CSSC-7SAT90-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/probSAT/probSATWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -luby '1' -cb1 '5.38125019852318' -fct '0' -randomc '0' -eps '0.9050979556211487' -xor '1' -caching '1' -base '50378' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/probSAT/probSATWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -luby '0' -cb2 '1.1157334857297916' -cb1 '3.8734883171825873' -fct '1' -randomc '1' -caching '0' SparrowToRiss CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -quickRed 'no' -minLBDMinimizingClause '5' -pr-probeL '2319745' -hack '1' -SPARROW-k 'yes' -longConflict 'no' -keepWorst '0.011050331636993038' -firstReduceDB '4226' -incLBD 'no' -lbdIgnL0 'yes' -hack-cost 'yes' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'yes' -vsids-i '1.0' -specialIncReduceDB '1100' -SPARROW--sp '0.48300324349338253' -sUHLEsize '0' -init-act '3' -pr-keepL '0' -varActB '0' -pr-keepI '0' -sInterval '2' -phase-saving '2' -var-decay-i '0.01' -alluiphack '2' -SPARROW--randomc '1' -vsids-s '1.0' -dontTrust 'no' -pr-lhbr 'no' -SPARROW--luby '0' -learnDecP '80' -pr-double 'no' -var-decay-e '0.95' -var-decay-d '15000' -var-decay-b '0.75' -actStart '2048.0' -lbdupd '1' -minLBDFrozenClause '15' -minSizeMinimizingClause '4' -cla-decay '0.5' -cp3_ee_bIter '45480738' -incReduceDB '379' -pr-uips '-1' -biAsFreq '15' -rlevel '2' -strFlips '-2' -SPARROW--c1 '2.2539544652678742' -clsActB '0' -init-pol '1' -pr-nce 'no' -rnd-freq '0.006291303829455201' CSSC-7SAT90-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -rer-minLBD '1' -sUhdPrRb 'yes' -quickRed 'no' -agil-r 'yes' -ics_dyn 'no' -ics_relSIZE '1.0' -minLBDMinimizingClause '8' -pr-probeL '665956' -hack '1' -SPARROW-k 'yes' -otfss 'no' -longConflict 'no' -keepWorst '0.03940593666730101' -firstReduceDB '3631' -strSseconds '150' -ics 'yes' -incLBD 'yes' -rer-maxLBD '30' -rinc '3.7361703315767123' -rer-max-size '2147483647' -lbdIgnL0 'yes' -hack-cost 'yes' -rer 'yes' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'no' -vsids-i '1.0' -ics_shrinkNew 'no' -rer-freq '0.5' -specialIncReduceDB '2000' -SPARROW--sp '0.7256996549106322' -rer-r '1' -sUHLEsize '8' -agil-add '512' -init-act '6' -pr-keepL '0' -varActB '1' -pr-keepI '2' -sInterval '1' -phase-saving '2' -var-decay-i '0.001' -rer-l 'yes' -sUHLElbd '6' -ics_relLBD '1.0' -alluiphack '0' -SPARROW--randomc '0' -rer-f 'no' -rer-min-size '15' -rtype '2' -vsids-s '1.0' -dontTrust 'yes' -pr-lhbr 'yes' -SPARROW--luby '0' -sUhdProbe '3' -learnDecP '66' -pr-double 'no' -var-decay-e '0.95' -var-decay-d '10000' -var-decay-b '0.75' -actStart '2048.0' -lbdupd '0' -minLBDFrozenClause '15' -minSizeMinimizingClause '45' -ics_processLast '50000' -agil-decay '0.9955803319496221' -cla-decay '0.999' -cp3_ee_bIter '1' -ics_keepNew 'no' -sUhdPrSh '2' -incReduceDB '373' -ics_window '10000' -pr-uips '1' -agil-limit '0.3273019196920353' -laHack 'no' -rlevel '0' -agil-init '0.07671016750064451' -strFlips '500000000' -enabled_cp3 'no' -SPARROW--c1 '6.806060972909069' -clsActB '2' -init-pol '2' -pr-nce 'yes' -lhbr '0' -rer-new-act '4' -rnd-freq '4.636117112213095E-5' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -sUhdPrRb 'no' -quickRed 'yes' -agil-r 'no' -minLBDMinimizingClause '5' -pr-probeL '4349652' -hack '0' -SPARROW-k 'yes' -otfss 'yes' -longConflict 'yes' -keepWorst '0.01807304625319327' -firstReduceDB '5338' -strSseconds '200' -ics 'no' -incLBD 'no' -lbdIgnL0 'yes' -rer 'no' -vsids-e '1.0' -vsids-d '2147483647' -lhbr-sub 'no' -biAsserting 'no' -vsids-i '1.0' -laEEp '100' -laEEl 'yes' -rfirst '771' -specialIncReduceDB '2000' -SPARROW--sp '0.7450345518096311' -hlaTop '-1' -sUHLEsize '30' -tabu 'yes' -otfssMLDB '2' -hlaevery '8' -init-act '4' -pr-keepL '0' -varActB '1' -pr-keepI '2' -sInterval '1' -phase-saving '0' -var-decay-i '0.001' -sUHLElbd '2' -alluiphack '2' -SPARROW--randomc '0' -hlaMax '320' -rtype '1' -vsids-s '1.0' -dontTrust 'yes' -otfssL 'yes' -pr-lhbr 'no' -SPARROW--luby '0' -hlaLevel '1' -sUhdProbe '1' -learnDecP '100' -pr-double 'yes' -var-decay-e '0.85' -var-decay-d '10000' -var-decay-b '0.75' -actStart '1024.0' -lbdupd '1' -minLBDFrozenClause '15' -minSizeMinimizingClause '4' -cla-decay '0.999' -cp3_ee_bIter '7331490' -sUhdPrSh '8' -incReduceDB '300' -pr-uips '1' -laHack 'yes' -rlevel '2' -dyn 'no' -strFlips '500000000' -enabled_cp3 'no' -hlabound '-1' -SPARROW--c1 '7.931983908669672' -clsActB '0' -lhbr-max '0' -init-pol '0' -pr-nce 'yes' -lhbr '4' -rnd-freq '0.0014229335991899667' CSCCSat2014 CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/CSCCSat2014/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -prob '0.65' -sp '0.77' -w_t '400' CSSC-7SAT90-sat-300s-2day bash run-algo.sh instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -prob '0.6' -sp '0.77' -w_t '700' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/CSCCSat2014/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -prob '0.6' -sp '0.82' -w_t '400' YalSAT CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -correct '0' -cacheduni '0' -best '0' -cachemax '1024' -pol '1' -defrag '0' -pick '3' -cached '1' -prep '1' -reluctant '1' -rbfsrate '1000' -minchunksize '256' -restart '100000' -unfairfreq '75' -restartouterfactor '1000' -weight '5' -hitlim '-1' -toggleuniform '0' -uni '1' -crit '1' -keep '0' -cachemin '0' -fixed '0' -unirestarts '1000' -unipick '-1' -geomfreq '66' -restartouter '0' CSSC-7SAT90-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -correct '0' -cacheduni '0' -best '1' -cachemax '1024' -pol '1' -defrag '0' -pick '0' -cached '0' -prep '1' -reluctant '1' -rbfsrate '100' -minchunksize '8129' -restart '10000' -unfairfreq '25' -restartouterfactor '100' -weight '3' -hitlim '-1' -toggleuniform '0' -uni '1' -crit '1' -keep '1' -cachemin '0' -fixed '32768' -unirestarts '100' -unipick '4' -geomfreq '55' -restartouter '1' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -correct '0' -cacheduni '0' -best '0' -cachemax '1044056' -pol '-1' -defrag '1' -pick '3' -cached '1' -prep '0' -reluctant '1' -rbfsrate '1' -minchunksize '350122' -restart '76207287' -unfairfreq '18' -restartouterfactor '1644' -weight '7' -hitlim '117555832' -toggleuniform '0' -uni '-1' -crit '1' -keep '1' -cachemin '635' -fixed '14574586' -unirestarts '1407079971' -unipick '4' -geomfreq '100' -restartouter '0' clasp-3.0.4-p8 CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -@1:F:update-act 'no' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@1:2:Geo:restarts '1.5' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:counter-restarts '3' -@1:rand-freq '0.0' -@1:update-lbd '0' -@1:3:deletion '0' -@1:0:strengthen 'local' -@1:1:lookahead 'no' -@1:del-max '250000' -@1:3:del-init '9000' -@1:save-progress '180' -@0:1:sat-prepro '10' -@0:5:sat-prepro '1' -@1:S:counterCond 'yes' -@1:init-watches '2' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '95' -@1:S:contraction 'no' -@1:sign-def '1' -@0:2:sat-prepro '25' -@1:0:del-cfl 'no' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:No:contraction 'no' -@1:2:del-init '1000' -@1:counter-bump '10' -@1:reverse-arcs '1' -@1:0:restarts 'x' -@1:S:Geo:aryrestarts '2' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:1:Simp:restarts '128' -@1:2:deletion '75' -@1:F:init-moms 'no' -@1:1:strengthen '0' CSSC-7SAT90-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -@1:F:update-act 'no' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@1:2:Geo:restarts '1.5' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:counter-restarts '3' -@1:rand-freq '0.0' -@1:update-lbd '0' -@1:3:deletion '0' -@1:0:strengthen 'local' -@1:1:lookahead 'no' -@1:del-max '250000' -@1:3:del-init '9000' -@1:save-progress '180' -@0:1:sat-prepro '10' -@0:5:sat-prepro '1' -@1:S:counterCond 'yes' -@1:init-watches '2' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '95' -@1:S:contraction 'no' -@1:sign-def '1' -@0:2:sat-prepro '25' -@1:0:del-cfl 'no' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:No:contraction 'no' -@1:2:del-init '1000' -@1:counter-bump '10' -@1:reverse-arcs '1' -@1:0:restarts 'x' -@1:S:Geo:aryrestarts '2' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:1:Simp:restarts '128' -@1:2:deletion '75' -@1:F:init-moms 'no' -@1:1:strengthen '0' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -@1:F:update-act 'no' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@1:2:Geo:restarts '1.5' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:counter-restarts '3' -@1:rand-freq '0.0' -@1:update-lbd '0' -@1:3:deletion '0' -@1:0:strengthen 'local' -@1:1:lookahead 'no' -@1:del-max '250000' -@1:3:del-init '9000' -@1:save-progress '180' -@0:1:sat-prepro '10' -@0:5:sat-prepro '1' -@1:S:counterCond 'yes' -@1:init-watches '2' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '95' -@1:S:contraction 'no' -@1:sign-def '1' -@0:2:sat-prepro '25' -@1:0:del-cfl 'no' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:No:contraction 'no' -@1:2:del-init '1000' -@1:counter-bump '10' -@1:reverse-arcs '1' -@1:0:restarts 'x' -@1:S:Geo:aryrestarts '2' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:1:Simp:restarts '128' -@1:2:deletion '75' -@1:F:init-moms 'no' -@1:1:strengthen '0' minisat-HACK-999ED-CSSC CSSC-3SAT1k-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/3sat1k.test/unif-k3-r4.26-v1000-c4260-S1934218998.cnf 0 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '5' -luby '0' -core-tolerance '0.02' -K-val '0.8' -cla-decay '0.999' -cp-increase '15000' -lbd-cut-max '10' -R-val '1.4' CSSC-7SAT90-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/7sat90.test/unif-k7-r85.00-v90-c7650-S665010681.cnf 0 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '5' -luby '0' -core-tolerance '0.02' -K-val '0.8' -cla-decay '0.999' -cp-increase '15000' -lbd-cut-max '10' -R-val '1.4' CSSC-5SAT500-sat-300s-2day python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '5' -luby '0' -core-tolerance '0.02' -K-val '0.8' -cla-decay '0.999' -cp-increase '15000' -lbd-cut-max '10' -R-val '1.4'