default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -@1:0:deletion '3' -@1:0:restarts 'x' -@1:0:restarts:del-cfl '+' -@1:1:Simp:restarts '128' -@1:1:del-algo 'basic' -@1:1:del-glue '2' -@1:1:del-grow '1.1' -@1:1:del-init-r '1000' -@1:1:del-on-restart '30' -@1:1:deletion '75' -@1:1:lookahead 'no' -@1:1:restarts:del-cfl '10000' -@1:1:sat-prepro '10' -@1:1:strengthen 'local' -@1:2:Ari:restarts:del-cfl '1000' -@1:2:Geo:restarts '1.5' -@1:2:del-algo '0' -@1:2:del-glue '0' -@1:2:del-grow '20.0' -@1:2:del-init-r '9000' -@1:2:deletion '10.0' -@1:2:sat-prepro '25' -@1:2:strengthen '0' -@1:3:restarts:del-grow 'L' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '1000' -@1:4:sat-prepro '100' -@1:5:sat-prepro '1' -@1:F:init-moms 'no' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:No:contraction 'no' -@1:S:Ari:aryrestarts:del-cfl '2' -@1:S:Geo:aryrestarts '2' -@1:S:Luby:aryrestarts:del-grow '1' -@1:S:contraction 'no' -@1:S:counterCond 'yes' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'yes' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:counter-bump '10' -@1:counter-restarts '3' -@1:del-max '32767' -@1:heuristic 'Vsids' -@1:init-watches '2' -@1:otfs '2' -@1:reverse-arcs '1' -@1:save-progress '180' -@1:sign-def '1' -@1:update-lbd '0' -@1:vsids-decay '70'
CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -@1:0:deletion '1' -@1:0:restarts '+' -@1:1:Simp:restarts '128' -@1:1:del-algo 'inp_sort' -@1:1:del-glue '7' -@1:1:del-grow '1.271838923530963' -@1:1:del-init-r '547' -@1:1:del-on-restart '0' -@1:1:deletion '54' -@1:1:lookahead 'body' -@1:1:sat-prepro '14' -@1:1:strengthen 'local' -@1:2:Ari:restarts '6' -@1:2:del-algo '1' -@1:2:del-glue '1' -@1:2:del-grow '56.69507530371241' -@1:2:del-init-r '16259' -@1:2:deletion '1.2998568802440595' -@1:2:lookahead '24' -@1:2:sat-prepro '14' -@1:2:strengthen '2' -@1:3:Ari:restarts '28516' -@1:3:restarts:del-grow 'L' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '1' -@1:4:sat-prepro '10' -@1:5:Luby:restarts:del-grow '1' -@1:5:sat-prepro '0' -@1:F:init-moms 'yes' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:No:contraction 'no' -@1:S:Ari:aryrestarts '3' -@1:S:Luby:aryrestarts:del-grow '2' -@1:S:contraction 'no' -@1:S:counterCond 'no' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'yes' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:del-max '88147269' -@1:heuristic 'Vsids' -@1:init-watches '0' -@1:otfs '0' -@1:reverse-arcs '1' -@1:save-progress '133' -@1:sign-def '2' -@1:update-lbd '0' -@1:vsids-decay '84'
CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -@1:0:deletion '3' -@1:0:restarts 'x' -@1:0:restarts:del-cfl '+' -@1:1:Simp:restarts '128' -@1:1:del-algo 'basic' -@1:1:del-glue '2' -@1:1:del-grow '1.1' -@1:1:del-init-r '1000' -@1:1:del-on-restart '30' -@1:1:deletion '75' -@1:1:lookahead 'no' -@1:1:restarts:del-cfl '1000' -@1:1:sat-prepro '10' -@1:1:strengthen 'local' -@1:2:Ari:restarts:del-cfl '1000' -@1:2:Geo:restarts '1.5' -@1:2:del-algo '0' -@1:2:del-glue '0' -@1:2:del-grow '20.0' -@1:2:del-init-r '9000' -@1:2:deletion '10.0' -@1:2:sat-prepro '25' -@1:2:strengthen '0' -@1:3:restarts:del-grow 'L' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '1000' -@1:4:sat-prepro '100' -@1:5:sat-prepro '1' -@1:F:init-moms 'no' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:No:contraction 'no' -@1:S:Ari:aryrestarts:del-cfl '2' -@1:S:Geo:aryrestarts '2' -@1:S:Luby:aryrestarts:del-grow '1' -@1:S:contraction 'no' -@1:S:counterCond 'yes' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'yes' -@1:counter-bump '10' -@1:counter-restarts '3' -@1:del-max '32767' -@1:heuristic 'Vsids' -@1:init-watches '2' -@1:otfs '2' -@1:reverse-arcs '1' -@1:save-progress '180' -@1:sign-def '1' -@1:solver './clasp' -@1:update-lbd '0' -@1:vsids-decay '70'
CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '1' -@1:0:restarts 'no' -@1:1:del-algo 'basic' -@1:1:del-glue '5' -@1:1:del-grow '1.0' -@1:1:del-init-r '500' -@1:1:del-on-restart '15' -@1:1:deletion '75' -@1:1:lookahead 'no' -@1:1:sat-prepro '10' -@1:1:strengthen 'recursive' -@1:2:del-algo '0' -@1:2:del-glue '1' -@1:2:del-grow '0.0' -@1:2:del-init-r '20000' -@1:2:deletion '10.0' -@1:2:sat-prepro '10' -@1:2:strengthen '1' -@1:3:restarts:del-grow 'F' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '4096' -@1:4:sat-prepro '-1' -@1:5:sat-prepro '2' -@1:F:init-moms 'yes' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:S:contraction 'yes' -@1:S:counterCond 'no' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'yes' -@1:contraction '120' -@1:del-max '20000' -@1:heuristic 'Vsids' -@1:init-watches '2' -@1:otfs '2' -@1:reverse-arcs '3' -@1:save-progress '50' -@1:sign-def '2' -@1:solver './clasp' -@1:update-lbd '0' -@1:vsids-decay '95'
CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '0' -@1:0:restarts 'L' -@1:1:Simp:restarts '128' -@1:1:del-on-restart '0' -@1:1:lookahead 'atom' -@1:1:strengthen 'local' -@1:2:Luby:restarts '10' -@1:2:lookahead '10' -@1:2:strengthen '1' -@1:F:init-moms 'no' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:S:Luby:aryrestarts '2' -@1:S:contraction 'yes' -@1:S:counterCond 'no' -@1:S:del-initCond 'no' -@1:S:sat-prepro 'no' -@1:contraction '120' -@1:heuristic 'None' -@1:init-watches '0' -@1:otfs '1' -@1:reverse-arcs '2' -@1:sat-prepro '0' -@1:save-progress '180' -@1:sign-def '2' -@1:solver './clasp' -@1:update-lbd '3'
CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '2' -@1:0:restarts 'D' -@1:0:restarts:del-cfl 'x' -@1:1:Dyn:restarts '128' -@1:1:del-algo 'sort' -@1:1:del-glue '2' -@1:1:del-on-restart '28' -@1:1:deletion '46' -@1:1:lookahead 'body' -@1:1:restarts:del-cfl '29091' -@1:1:sat-prepro '2' -@1:1:strengthen 'recursive' -@1:2:Dyn:restarts '0.9171244474401926' -@1:2:Geo:restarts:del-cfl '1.116644361570374' -@1:2:del-algo '0' -@1:2:del-glue '0' -@1:2:deletion '7.053547411640475' -@1:2:lookahead '6386' -@1:2:sat-prepro '19' -@1:2:strengthen '0' -@1:3:Dyn:restarts '119' -@1:3:Geo:restarts:del-cfl '2083' -@1:3:sat-prepro '-1' -@1:4:sat-prepro '4' -@1:5:sat-prepro '2' -@1:F:init-moms 'yes' -@1:F:local-restarts 'yes' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:No:contraction 'no' -@1:S:Dyn:aryrestarts '3' -@1:S:Geo:aryrestarts:del-cfl '3' -@1:S:contraction 'no' -@1:S:counterCond 'yes' -@1:S:del-initCond 'no' -@1:S:sat-prepro 'yes' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:counter-bump '15' -@1:counter-restarts '99' -@1:heuristic 'Vsids' -@1:init-watches '2' -@1:otfs '1' -@1:reverse-arcs '3' -@1:save-progress '164' -@1:sign-def '2' -@1:update-lbd '0' -@1:vsids-decay '97'
CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '3' -@1:0:restarts '+' -@1:0:restarts:del-cfl 'x' -@1:1:Simp:restarts '1' -@1:1:del-algo 'sort' -@1:1:del-glue '6' -@1:1:del-grow '1.964690937254872' -@1:1:del-init-r '8' -@1:1:del-on-restart '1' -@1:1:deletion '79' -@1:1:lookahead 'body' -@1:1:restarts:del-cfl '6186' -@1:1:sat-prepro '16' -@1:1:strengthen 'recursive' -@1:2:Ari:restarts '258' -@1:2:Geo:restarts:del-cfl '1.7378851086623572' -@1:2:del-algo '1' -@1:2:del-glue '1' -@1:2:del-grow '94.80400305060496' -@1:2:del-init-r '24962' -@1:2:deletion '6.069596664988586' -@1:2:lookahead '6' -@1:2:sat-prepro '1' -@1:2:strengthen '1' -@1:3:Ari:restarts '169' -@1:3:Geo:restarts:del-cfl '661' -@1:3:restarts:del-grow 'F' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '48093' -@1:4:sat-prepro '13' -@1:5:sat-prepro '2' -@1:F:init-moms 'yes' -@1:F:local-restarts 'no' -@1:F:sign-fix 'no' -@1:F:update-act 'no' -@1:No:contraction 'no' -@1:S:Ari:aryrestarts '3' -@1:S:Geo:aryrestarts:del-cfl '3' -@1:S:contraction 'no' -@1:S:counterCond 'yes' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'yes' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:counter-bump '176' -@1:counter-restarts '43' -@1:del-max '1351183063' -@1:heuristic 'Vsids' -@1:init-watches '2' -@1:otfs '1' -@1:reverse-arcs '1' -@1:save-progress '0' -@1:sign-def '1' -@1:update-lbd '0' -@1:vsids-decay '88'
CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '1' -@1:0:restarts 'no' -@1:1:del-algo 'sort' -@1:1:del-glue '1' -@1:1:del-grow '1.033794345701214' -@1:1:del-init-r '381' -@1:1:del-on-restart '45' -@1:1:deletion '72' -@1:1:lookahead 'no' -@1:1:strengthen 'local' -@1:2:del-algo '0' -@1:2:del-glue '1' -@1:2:del-grow '49.455110130265496' -@1:2:del-init-r '16667' -@1:2:deletion '5.0141635675108995' -@1:2:strengthen '1' -@1:3:restarts:del-grow 'x' -@1:4:restarts:del-grow '9773' -@1:5:Geo:restarts:del-grow '1.267769586650365' -@1:6:Geo:restarts:del-grow '263' -@1:F:berk-huang 'yes' -@1:F:berk-once 'no' -@1:F:init-moms 'yes' -@1:F:local-restarts 'yes' -@1:F:sign-fix 'no' -@1:F:update-act 'yes' -@1:S:Geo:aryrestarts:del-grow '3' -@1:S:contraction 'yes' -@1:S:counterCond 'no' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'no' -@1:berk-max '2' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:contraction '92' -@1:del-max '431789641' -@1:heuristic 'Berkmin' -@1:init-watches '2' -@1:otfs '0' -@1:reverse-arcs '0' -@1:sat-prepro '0' -@1:save-progress '169' -@1:sign-def '0' -@1:update-lbd '0'
CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '3' -@1:0:restarts 'no' -@1:0:restarts:del-cfl 'F' -@1:1:del-algo 'basic' -@1:1:del-glue '0' -@1:1:del-grow '1.0' -@1:1:del-on-restart '15' -@1:1:deletion '66' -@1:1:lookahead 'hybrid' -@1:1:restarts:del-cfl '32' -@1:1:sat-prepro '50' -@1:1:strengthen 'local' -@1:2:del-algo '0' -@1:2:del-glue '0' -@1:2:del-grow '1.0' -@1:2:deletion '2.0' -@1:2:lookahead '1' -@1:2:sat-prepro '-1' -@1:2:strengthen '2' -@1:3:restarts:del-grow 'x' -@1:3:sat-prepro '-1' -@1:4:restarts:del-grow '256' -@1:4:sat-prepro '100' -@1:5:Geo:restarts:del-grow '1.3' -@1:5:sat-prepro '2' -@1:6:Geo:restarts:del-grow '100' -@1:F:berk-huang 'yes' -@1:F:berk-once 'no' -@1:F:init-moms 'yes' -@1:F:local-restarts 'yes' -@1:F:sign-fix 'no' -@1:F:update-act 'yes' -@1:S:Geo:aryrestarts:del-grow '3' -@1:S:contraction 'yes' -@1:S:counterCond 'yes' -@1:S:del-initCond 'no' -@1:S:sat-prepro 'yes' -@1:berk-max '128' -@1:contraction '200' -@1:heuristic 'Berkmin' -@1:init-watches '2' -@1:otfs '0' -@1:reverse-arcs '0' -@1:save-progress '1' -@1:sign-def '0' -@1:solver './clasp' -@1:update-lbd '0'
CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb clasp-cssc instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -@1:0:deletion '3' -@1:0:restarts 'no' -@1:0:restarts:del-cfl 'L' -@1:1:del-algo 'basic' -@1:1:del-glue '5' -@1:1:del-grow '4.945291149057953' -@1:1:del-init-r '2' -@1:1:del-on-restart '8' -@1:1:deletion '57' -@1:1:lookahead 'no' -@1:1:restarts:del-cfl '180' -@1:1:strengthen 'local' -@1:2:del-algo '1' -@1:2:del-glue '0' -@1:2:del-grow '68.8142558508613' -@1:2:del-init-r '21233' -@1:2:deletion '5.893662247065181' -@1:2:strengthen '1' -@1:3:restarts:del-grow '+' -@1:4:restarts:del-grow '6' -@1:5:Ari:restarts:del-grow '4108' -@1:6:Ari:restarts:del-grow '2003' -@1:F:berk-huang 'no' -@1:F:berk-once 'yes' -@1:F:init-moms 'no' -@1:F:local-restarts 'yes' -@1:F:sign-fix 'no' -@1:F:update-act 'yes' -@1:S:Ari:aryrestarts:del-grow '3' -@1:S:Luby:aryrestarts:del-cfl '1' -@1:S:contraction 'yes' -@1:S:counterCond 'yes' -@1:S:del-initCond 'yes' -@1:S:sat-prepro 'no' -@1:berk-max '121' -@1:clasp:prefix '--' -@1:clasp:solver './clasp' -@1:contraction '747' -@1:del-max '1504270188' -@1:heuristic 'Berkmin' -@1:init-watches '0' -@1:otfs '0' -@1:reverse-arcs '0' -@1:sat-prepro '0' -@1:save-progress '116' -@1:sign-def '2' -@1:update-lbd '3'