#!/bin/sh # Usage: vallstSAT2005PB.sh problemfile seed [vallstoptions] # Repeatedly calls vallst to solve a boolean constraint problem. # Like vallst.sh but conforms to the requirements in the SAT 2005 # pseudo boolean competitions. (You might want change the value of vallstcom # below.) You can add the option --pb=no (last) if you want to use the script # on non (o)pb files. # Exit values: # 20: A proof of false was found. # 10: A model was found. No proof that it is optimal was found. # 0: The time limit has been exceeded. Not used here. # 0: An interupt signal was received and no result at all was obtained. # 4: Not enough memory could be allocated. # 5: Some file error occurred. # 30: Optimal value/model found. # vallstoptions are the usual vallst options, see vallst --help, with the # following exceptions: # * It must not contain an unflagged problemfile. ( --file can be used but # will have no effect.) # * Any time limit will only affect vallst calls; there is no time limit for # the script itself. You can kill the script in a controlled manner with # ctrl-c (SIGINT) or a term signal (SIGTERM) or SIGXCPU to the vallst # process. It might be better to signal or kill the subprocess vallst # rather than the script ($$) if you want to quit. # * These flags will be overridden and will have no effect: # --out-theory-file-name --changing-setting-file-name # --var-map-file-name. # * These flags will only affect the first vallst call: # --first-restart --nr-of-vars-set-at-start-is-zero. # * Any --seed option will be overwritten by the script's seed option ($2). #set -x # The directory where temporary files are saved. Any model is also saved here. # Posibly defined previously. #tmpdir="/tmp" if [ -z "$tmpdir" ] then tmpdir="/tmp" fi # Name to evoke vallst with. # Posibly defined previously. #vallstcom=vallst if [ -z "$vallstcom" ] then vallstcom=vallst fi # Time limit for subcalls in seconds. Not used. #timeLimit=600 firstrestart=80 # Every period-th time, we will try evoking the solver with a bit different # options. On those more rare occasions we will focus more on simplification. period=4 # Kill any child. Flawed because it kills its own subprocess!!?? function killchild { ps -o pid= -o ppid= -o comm= | while read pid ppid comm do if [ "$ppid" -eq "$$" ] && [ "$comm" == "vallst" ] then kill -s SIGINT $pid fi done } # Redirect all output heading to stdout to stderr. exec 8>&1 # Get a name for the real stdout. exec 1>&2 #exec 1>/dev/null #exec 9>&2 # Get a name for the real stderr. #exec 2>/dev/null # Make sure that tmpdir exists. Is this a good practice?? mkdir -p $tmpdir # Find a unique temporary subdirectory name to be used for this call. # Nr of other current simultaneous runs made. The tmp subdir will be named # ${tmpdir}/vallst_sh_tmp_subdir_${d}. d=0 mkdir ${tmpdir}/vallst_sh_tmp_subdir_${d} dres=$? while [ $dres -ne 0 ] do let d+=1 if [ $d -eq 1000 ] then echo "Error: cannot create a new temp dir ${tmpdir}/vallst_sh_tmp_subdir_n" exit 5 fi mkdir ${tmpdir}/vallst_sh_tmp_subdir_${d} dres=$? done # Holds the result of vallst calls. result=3 # Copy files in tmpdir that should be saved to its parent. function copyfiles { if [ $result -eq 3 ] then echo " Interupt; Current theory and settings are copied here:" 1>&2 echo " ${tmpdir}/vallst_sh_out_theory.vnf" 1>&2 echo " ${tmpdir}/vallst_sh_changing_setting.options" 1>&2 wait nice \ cp -f -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ ${tmpdir}/vallst_sh_out_theory.vnf cp -f -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ ${tmpdir}/vallst_sh_changing_setting.options fi } # Clean up if the script is terminated ungracefully. # Note that SIGINT, SIGTERM and SIGXCPU are handled also by vallst. # We'll also kill any subprocess. # Handling specific signals isn't working as intended because the script # will wait until any vallst call is finished before dealing with any signal # sent to the script. How to fix this????? The way the code works now, not # trapping any signals except at exit, is perhaps good enough though. The trap # will execute at every exit even though it's only when a signal was sent to # the parent, $$, that it is useful. However, wait isn't working!! Hence the # "sleep 0.3". #trap killchild SIGXCPU #trap killchild SIGINT #trap killchild SIGTERM trap ' killchild; wait; sleep 0.3; wait; copyfiles; \ rm -f -r ${tmpdir}/vallst_sh_tmp_subdir_${d} ' EXIT seed=$2 problemfile=$1 shift shift # Number of vallst calls made, also counting the coming one. n=1 echo "$n:" $vallstcom \ --pb \ --complete-model=yes \ --first-restart=$firstrestart \ --improve-proof-level=0 \ --abort-threshold=60 \ --no-abort-time=300 \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ --nr-of-vars-set-at-start-is-zero=yes \ "$@" \ --seed=$seed $problemfile \ --var-map-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options result=$? # Fix problem with conversion of pb format to the internal format. This will # hardly ever happen. # Check if false was proved and no model found and if the problem is a pb # problem. function fixAllFalseOpt { if [ $result -eq 0 ] && [ ! -s ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model ] && [ -s ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map ] then # Check if the problem is an optimizing one. This is a hack. grep "min:" $problemfile > /dev/null grepres = $? if [ $grepres -eq 0 ] then echo "min problem does not have a model where any objective lit is false!" # Strip the problem of the objective formula. sed -e "/*min:*/d" $problemfile > ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_non_min_problem.pb # Add all literals in the min formula as true. # temp exit!!!!!vvvv finish!!!!!!!!!!vvvvvvvvvvvvvvv echo "Will exit with value 0! Finish code!!!!!!!!vvvvvvvvvv" exit 0 # finish!!!!!!!!!!!!!!vvvvvvvvvvvvvvvvvvv # Solve the stripped problem. $vallstcom \ --pb \ --complete-model=yes \ --first-restart=$firstrestart \ --improve-proof-level=0 \ --abort-threshold=60 \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ --nr-of-vars-set-at-start-is-zero=yes \ "$@" \ --seed=$seed \ ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_non_min_problem.pb \ --var-map-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options result=$? # Exit.? # finish!!!!!!!!!!!!!!vvvvvvvvvvvvvvvvvvv fall through? fi fi } #fixAllFalseOpt # Used to store the value of n%$period (because I suck at script programming). p=0 while [ $result -eq 2 ] do #cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf ${tmpdir}/vallst_sh_out_theory$n.vnf let n+=1 let firstrestart+=40 let p=$n%$period echo echo "$n:" if [ $p -eq 0 ] then $vallstcom \ --complete-model=yes \ --improve-proof-level=999999 \ --simp-time-limit-fast=3800 --simp-time-limit-slow=100000 \ --simp-setting 1-1-4294901498-0 --simp-setting 2-1-400-0 \ --simp-setting 2-2-40-0 --simp-setting 3-1-60-0 \ --simp-setting 3-2-8-0 --simp-setting 3-3-6-0 \ --simp-setting-slow 1-1-4294901501-0 \ --simp-setting-slow 2-1-2200-0 --simp-setting-slow 2-2-348-0 \ --simp-setting-slow 3-1-200-0 --simp-setting-slow 3-2-16-0 \ --simp-setting-slow 3-3-7-0 --simp-setting-slow 4-1-14-0 \ --simp-setting-slow 4-2-6-0 --simp-setting-slow 4-3-4-0 \ --simp-setting-slow 4-4-3-0 \ --abort-threshold=50 \ --no-abort-time=240 \ --subst-equs=no \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ "$@" \ --pb=no --atsp=no --tsp=no \ --seed=$seed \ --nr-of-vars-set-at-start-is-zero=no \ --time-limit=360 \ --first-restart=$firstrestart \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ --file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ $(head --lines=1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options) result=$? else $vallstcom \ --complete-model=yes \ --improve-proof-level=0 \ --abort-threshold=50 \ --no-abort-time=240 \ --subst-equs=no \ --result-file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ "$@" \ --pb=no --atsp=no --tsp=no \ --seed=$seed \ --nr-of-vars-set-at-start-is-zero=no \ --first-restart=$firstrestart \ --out-theory-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ --changing-setting-file-name=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options \ --file=${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_out_theory.vnf \ $(head --lines=1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_changing_setting.options) result=$? fi done fixAllFalseOpt echo "times:" times # Restore stdout. exec 1>&8 8>&- # Also closes the tmp name (8). #exec 2>&9 9>&- # Exit value. satresult=0 # The size of the variable map file. If it is larger than 2 bytes, then it # contains a full variable mapping. Otherwise the --char-prefix-pb-var option # was in effect and the file contains just the prefix character. varmapfilesize=0 # The prefix character when --char-prefix-pb-var is active. prefixChar="" function printpbmodel { varmapfilesize=$(wc -c < ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map) if [ $varmapfilesize -lt 3 ] then prefixChar=$(head -c 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map) str=$(tail -n 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model | \ sed -e "s/-/-$prefixChar/g" \ -e "s/ 1/ ${prefixChar}1/g" \ -e "s/ 2/ ${prefixChar}2/g" \ -e "s/ 3/ ${prefixChar}3/g" \ -e "s/ 4/ ${prefixChar}4/g" \ -e "s/ 5/ ${prefixChar}5/g" \ -e "s/ 6/ ${prefixChar}6/g" \ -e "s/ 7/ ${prefixChar}7/g" \ -e "s/ 8/ ${prefixChar}8/g" \ -e "s/ 9/ ${prefixChar}9/g" ) echo "v $str" else # Set up fds. exec 4<>${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map # Extract the last model and split literals into separate lines. tail -n 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model | \ sed -e "s/ -/\n-/g" -e "s/ /\n/g" > \ ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_last.model exec 5<>${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh_last.model echo -n "v " while read -u 4 var do read -u 5 mod if [[ $mod == -* ]] then echo -n "-$var " else echo -n " $var " fi done # Close fds. exec 4>&- exec 5>&- echo fi } function printmodel { if [ -s ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map ] then cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_var_map \ ${tmpdir}/vallst_var_map printpbmodel else echo "v $(tail -n 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model)" fi } if [ $result -eq 0 ] then # Detect if there is a non-empty model file. if [ -s ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model ] then cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ ${tmpdir}/vallst_sh.model printmodel #echo "v $(tail -n 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model)" #echo "v 0" echo "s OPTIMUM FOUND" let satresult=30 else echo "s UNSATISFIABLE" let satresult=20 fi fi if [ $result -eq 1 ] then cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ ${tmpdir}/vallst_sh.model printmodel #echo "v $(cat ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model)" #echo "v 0" echo "s SATISFIABLE" let satresult=10 fi if [ $result -eq 3 ] then # Detect if there is a non-empty model file. if [ -s ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model ] then cp -p ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model \ ${tmpdir}/vallst_sh.model printmodel #echo "v $(tail -n 1 ${tmpdir}/vallst_sh_tmp_subdir_${d}/vallst_sh.model)" #echo "v 0" echo "s SATISFIABLE" let satresult=10 fi fi # Handle search assumptions (from --make-search-assumption) better!!?? if [ $satresult -eq 0 ] then echo "s UNKNOWN" if [ $result -eq 4 ] then let satresult=4 fi if [ $result -eq 5 ] then let satresult=5 fi fi # Below code is commented away because the exit is always trapped and things # are cleaned up there. If trapping is fixed so that signals are just # propagated (which is the ideal), uncomment below code!! #wait #rm -f -r ${tmpdir}/vallst_sh_tmp_subdir_${d} exit $satresult
Generated on Mon Jul 18 11:34:15 2005 for Vallst by doxygen 1.4.3.