FAMILIAR-project / usampling-exp

Uniform, random sampling: large study and results of different SAT-based samplers
4 stars 5 forks source link

DBS unknown exception handling #11

Open FAMILIAR-project opened 4 years ago

FAMILIAR-project commented 4 years ago

Unknown case badly managed: https://github.com/FAMILIAR-project/usampling-exp/blob/master/usampling-experiments.py#L480-L482 (basically the CSV row is not added)

so beware that some results with DBS 180 timeout or 90 might miss a few entries I've found only one: blaster_case123

based on the logs (pushed in the repo)

FAMILIAR-project commented 4 years ago

we have again this case with /home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf on large-scale results... https://github.com/FAMILIAR-project/usampling-exp/blob/master/usampling-data/results-timeout180/job.7765.output#L4905-L4908

FAMILIAR-project commented 4 years ago

docker run -it -v $(pwd):/home/usampling-exp -v $(pwd)/fmlinux:/home/fm_history_linux_dimacs/ macher/usampling:squashed /bin/bash -c 'cd /home/usampling-exp/; python3 usampling-experiments.py -t 100 --dbs -flas /home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf'


loading packages...
parsing arguments
starting usampling bench
formulas to process explicitly given ['/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf']
individual formula /home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf
1 formulas to process ['/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf']
DBS experiment
/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf
TIMEOUT
end of benchmarks
 mathieuacher  localhost.localdomain  ../usampling-exp  master △  cat usampling-data/experiments-DBS.csv
formula_file,execution_time_in,timeout,exception_dbs
/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf,100,True,False
FAMILIAR-project commented 4 years ago
docker run -it -v $(pwd):/home/usampling-exp -v $(pwd)/fmlinux:/home/fm_history_linux_dimacs/ macher/usampling:squashed /bin/bash -c 'cd /home/usampling-exp/; python3 usampling-experiments.py -t 300 --dbs -flas /home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf' 
loading packages...
parsing arguments
starting usampling bench
formulas to process explicitly given ['/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf']
individual formula /home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf
1 formulas to process ['/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf']
DBS experiment
/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf
still alive, DONE! command: log /tmp/output.txt

end of benchmarks

 mathieuacher  localhost.localdomain  ../usampling-exp  master △  cat usampling-data/experiments-DBS.csv
formula_file,timeout,execution_time_in,exception_dbs
/home/samplingfm/Benchmarks/Blasted_Real/blasted_case123.cnf,False,153.06793522834778,False