default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.4' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -fm 'no' -gc-frac '0.2' -hack '1' -hack-cost 'yes' -hte 'no' -incReduceDB '300' -init-act '0' -init-pol '0' -inprocess 'no' -laHack 'no' -learnDecP '100' -lhbr '0' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -otfss 'no' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -symm 'no' -szLBDQueue '50' -szTrailQueue '5000' -unhide 'yes' -up 'yes' -updLearnAct 'yes' -var-decay '0.95' -vmtf 'no' -xor 'no'
CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -3resolve 'yes' -K '0.7' -R '2.0' -alluiphack '2' -bva 'no' -bve 'yes' -bve_BCElim 'no' -bve_cgrow '10' -bve_cgrow_t '10000' -bve_gates 'no' -bve_heap_updates '1' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'yes' -bve_unlimited 'no' -cce 'yes' -ccmin-mode '0' -cla-decay '0.995' -cp3_bve_heap '1' -cp3_bve_inpInc '50000' -cp3_bve_learnt_growth '0' -cp3_bve_limit '25000000' -cp3_bve_resolve_learnts '2' -cp3_cce_inpInc '60000' -cp3_cce_level '1' -cp3_cce_sizeP '80' -cp3_cce_steps '3000000' -cp3_hte_inpInc '60000' -cp3_hte_steps '2147483' -cp3_inp_cons '80000' -cp3_itechs '"up"' -cp3_ptechs '"u3svghpwcv"' -cp3_randomized 'no' -cp3_res3_ncls '100000' -cp3_res3_reAdd 'no' -cp3_res3_steps '100000' -cp3_res_bin 'yes' -cp3_res_eagerSub 'yes' -cp3_res_inpInc '2000' -cp3_rew_1st 'no' -cp3_rew_Addlimit '10000' -cp3_rew_Vlimit '1000000' -cp3_rew_limit '120000' -cp3_rew_min '2' -cp3_rew_minA '13' -cp3_rew_ratio 'yes' -cp3_viv_inpInc '100000' -dense 'no' -dyn 'no' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '2000' -fm 'no' -gc-frac '0.1' -hack '1' -hack-cost 'yes' -hlaLevel '3' -hlaTop '64' -hlabound '-1' -hlaevery '8' -hte 'yes' -inc-inp 'yes' -incReduceDB '450' -init-act '2' -init-pol '0' -inprocess 'yes' -laHack 'yes' -learnDecP '100' -lhbr '4' -lhbr-max '20000000' -lhbr-sub 'yes' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '3' -minSizeMinimizingClause '30' -otfss 'no' -phase-saving '1' -pr-csize '4' -pr-probe 'no' -pr-vivi 'yes' -pr-viviL '5000000' -pr-viviP '60' -probe 'yes' -rMax '-1' -randInp 'no' -rew 'yes' -rnd-freq '0.5' -rtype '0' -sls 'yes' -sls-adopt-cls 'yes' -sls-ksat-flips '2000000000' -sls-rnd-walk '4000' -specialIncReduceDB '900' -subsimp 'no' -sym-clLearn 'yes' -sym-cons '0' -sym-consT '1000' -sym-iter '0' -sym-min '4' -sym-prop 'yes' -sym-propA 'yes' -sym-propF 'no' -sym-ratio '0.3' -sym-size 'yes' -symm 'yes' -szLBDQueue '70' -szTrailQueue '6000' -tabu 'yes' -unhide 'no' -up 'yes' -updLearnAct 'yes' -var-decay '0.85' -vmtf 'no' -xor 'no'
CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.4' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -fm 'no' -gc-frac '0.2' -hack '1' -hack-cost 'yes' -hte 'no' -incReduceDB '300' -init-act '0' -init-pol '0' -inprocess 'no' -laHack 'no' -learnDecP '100' -lhbr '0' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -otfss 'no' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -symm 'no' -szLBDQueue '50' -szTrailQueue '5000' -unhide 'yes' -up 'yes' -updLearnAct 'yes' -var-decay '0.95' -vmtf 'no' -xor 'no'
CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -3resolve 'no' -all_strength_res '0' -alluiphack '2' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_gates 'no' -bve_heap_updates '2' -bve_red_lits '1' -bve_strength 'no' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.995' -cp3_bve_heap '1' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ee_bIter '400000000' -cp3_ee_it 'no' -cp3_ee_limit '1000000' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '3000000' -cp3_strength 'no' -cp3_sub_limit '3000000' -cp3_uhdIters '1' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'yes' -ee_reset 'yes' -ee_sub 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -fm 'no' -gc-frac '0.2' -hack '0' -hte 'no' -incReduceDB '300' -init-act '0' -init-pol '0' -inprocess 'no' -laHack 'no' -learnDecP '66' -lhbr '0' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '9' -minSizeMinimizingClause '30' -otfss 'no' -phase-saving '2' -probe 'no' -rew 'no' -rfirst '100' -rinc '3' -rnd-freq '0' -rtype '2' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -symm 'no' -unhide 'yes' -up 'yes' -updLearnAct 'yes' -var-decay '0.99' -vmtf 'no' -xor 'no'
CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -alluiphack '2' -ccmin-mode '2' -cla-decay '0.995' -enabled_cp3 'no' -firstReduceDB '2000' -gc-frac '0.3' -hack '0' -incReduceDB '200' -init-act '0' -init-pol '5' -laHack 'no' -learnDecP '75' -lhbr '3' -lhbr-max '200000' -lhbr-sub 'no' -longConflict 'no' -minLBDFrozenClause '15' -minLBDMinimizingClause '9' -minSizeMinimizingClause '50' -otfss 'yes' -otfssL 'yes' -otfssMLDB '16' -phase-saving '2' -rfirst '1' -rnd-freq '0.5' -rtype '1' -specialIncReduceDB '900' -updLearnAct 'yes' -var-decay '0.85' -vmtf 'yes'
CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -K '0.7' -R '1.6' -alluiphack '2' -ccmin-mode '2' -cla-decay '0.995' -enabled_cp3 'no' -firstReduceDB '8000' -gc-frac '0.1' -hack '0' -incReduceDB '450' -init-act '3' -init-pol '4' -laHack 'no' -learnDecP '100' -lhbr '1' -lhbr-max '20000000' -lhbr-sub 'no' -longConflict 'yes' -minLBDFrozenClause '15' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -otfss 'yes' -otfssL 'yes' -otfssMLDB '30' -phase-saving '2' -rMax '10000' -rMaxInc '2' -rnd-freq '0' -rtype '0' -specialIncReduceDB '900' -szLBDQueue '70' -szTrailQueue '4000' -updLearnAct 'yes' -var-decay '0.85' -vmtf 'no'
CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -K '0.8' -R '1.6' -alluiphack '2' -ccmin-mode '2' -cla-decay '0.5' -dyn 'yes' -enabled_cp3 'no' -firstReduceDB '8000' -gc-frac '0.3' -hack '1' -hack-cost 'yes' -hlaLevel '4' -hlaMax '75' -hlaTop '64' -hlabound '1024' -hlaevery '64' -incReduceDB '300' -init-act '5' -init-pol '5' -laHack 'yes' -learnDecP '75' -lhbr '3' -lhbr-max '2000000' -lhbr-sub 'no' -longConflict 'no' -minLBDFrozenClause '50' -minLBDMinimizingClause '6' -minSizeMinimizingClause '50' -otfss 'yes' -otfssL 'no' -otfssMLDB '30' -phase-saving '0' -rMax '10000' -rMaxInc '2' -rnd-freq '0.5' -rtype '0' -specialIncReduceDB '900' -szLBDQueue '30' -szTrailQueue '4000' -tabu 'no' -updLearnAct 'yes' -var-decay '0.95' -vmtf 'no'
CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -alluiphack '0' -ccmin-mode '2' -cla-decay '0.995' -enabled_cp3 'no' -firstReduceDB '4000' -gc-frac '0.3' -hack '1' -hack-cost 'no' -incReduceDB '200' -init-act '1' -init-pol '1' -laHack 'no' -learnDecP '75' -lhbr '1' -lhbr-max '2000000' -lhbr-sub 'yes' -longConflict 'yes' -minLBDFrozenClause '15' -minLBDMinimizingClause '3' -minSizeMinimizingClause '15' -otfss 'no' -phase-saving '1' -rfirst '100' -rinc '3' -rnd-freq '0' -rtype '2' -specialIncReduceDB '1000' -updLearnAct 'yes' -var-decay '0.99' -vmtf 'no'
CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -3resolve 'yes' -K '0.5' -R '1.2' -alluiphack '0' -bva 'yes' -bve 'no' -cce 'no' -ccmin-mode '0' -cla-decay '0.999' -cp3_Abva 'no' -cp3_Ibva '2' -cp3_Ibva_heap '7' -cp3_Xbva '0' -cp3_bva_Ilimit '10000' -cp3_bva_Vlimit '3000000' -cp3_bva_incInp '20000' -cp3_ee_bIter '1' -cp3_ee_it 'no' -cp3_ee_limit '100000' -cp3_fm_1st 'no' -cp3_fm_amt 'no' -cp3_fm_cut 'yes' -cp3_fm_dups 'yes' -cp3_fm_grow '40' -cp3_fm_growT '100000' -cp3_fm_keepM 'yes' -cp3_fm_limit '1200000' -cp3_fm_merge 'no' -cp3_fm_newAlk '0' -cp3_fm_newAlo '0' -cp3_fm_newAmo '0' -cp3_fm_newSub 'no' -cp3_fm_unit 'no' -cp3_ptechs '"u3svghpwc"' -cp3_randomized 'yes' -cp3_res3_ncls '100000' -cp3_res3_reAdd 'no' -cp3_res3_steps '2000000' -cp3_res_bin 'yes' -cp3_res_eagerSub 'no' -cp3_res_inpInc '200000' -cp3_rew_1st 'no' -cp3_rew_Addlimit '200000' -cp3_rew_Vlimit '100000' -cp3_rew_limit '1200000' -cp3_rew_min '2' -cp3_rew_minA '2' -cp3_rew_ratio 'no' -dense 'no' -ee 'yes' -ee_reset 'no' -ee_sub 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -fm 'yes' -gc-frac '0.2' -hack '0' -hte 'no' -incReduceDB '200' -init-act '0' -init-pol '0' -inprocess 'no' -laHack 'no' -learnDecP '66' -lhbr '0' -longConflict 'no' -minLBDFrozenClause '50' -minLBDMinimizingClause '6' -minSizeMinimizingClause '3' -otfss 'yes' -otfssL 'yes' -otfssMLDB '128' -phase-saving '1' -pr-csize '2' -pr-probe 'no' -pr-vivi 'yes' -pr-viviL '5000000' -pr-viviP '80' -probe 'yes' -rMax '-1' -rew 'yes' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '900' -subsimp 'no' -sym-clLearn 'yes' -sym-cons '10' -sym-consT '10000' -sym-iter '0' -sym-min '1' -sym-prop 'yes' -sym-propA 'no' -sym-propF 'no' -sym-ratio '0.8' -sym-size 'no' -symm 'yes' -szLBDQueue '50' -szTrailQueue '6000' -unhide 'no' -up 'yes' -updLearnAct 'yes' -var-decay '0.99' -vmtf 'no' -xor 'yes' -xorFindSubs 'no' -xorKeepUsed 'no' -xorLimit '120000' -xorMaxSize '15' -xorSelect '1'
CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3gExt instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -alluiphack '2' -ccmin-mode '0' -cla-decay '0.5' -enabled_cp3 'no' -firstReduceDB '8000' -gc-frac '0.2' -hack '0' -incReduceDB '200' -init-act '3' -init-pol '2' -laHack 'no' -learnDecP '66' -lhbr '0' -longConflict 'no' -minLBDFrozenClause '15' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -otfss 'no' -phase-saving '2' -rfirst '1000' -rinc '3' -rnd-freq '0' -rtype '2' -specialIncReduceDB '1100' -updLearnAct 'yes' -var-decay '0.7' -vmtf 'no'