#import gbl import re import sys import argparse LARGEPOS=10000 LARGENEG=-10000 parser = argparse.ArgumentParser(description='Optional app description') parser.add_argument("-f", "--file", dest="myFilenameVariable", help="write report to FILE", metavar="FILE") parser.add_argument("-Csize", type=float, dest="Csize", default=0, help="Importance of the size of clauses") parser.add_argument("-CfirstNeg", type=int, dest="CfirstNeg", default=0, help="Importance of first literal as negative") ##lavorano come categorici -- 1 importante, 0 frega niente, -1 devi abbattere. parser.add_argument("-Cbinary", type=int, dest="Cbinary", default=0, help="Importance of binary clauses") ##lavorano come categorici -- 1 importante, 0 frega niente, -1 devi abbattere. parser.add_argument("-Cternary", type=int, dest="Cternary", default=0, help="Importance of ternary clauses") ##lavorano come categorici --1 importante, 0 frega niente, -1 devi abbattere. parser.add_argument("-CnumPosLit", type=float, dest="CposLit", default=0, help="Importance of positive literals in clauses") parser.add_argument("-CnumNegLit", type=float, dest="CnegLit", default=0, help="Importance of negative literals in clauses") parser.add_argument("-Cmutex", type=float, dest="Cmutex", default=0, help="Importance of mutex vars in clauses") parser.add_argument("-CnumVarInBin", type=float, dest="CnumVarBin", default=0, help="Order earlier clauses including clauses involved in binary") parser.add_argument("-CorderingAccordingVars", type=int, default=0, dest="CorderV", help="Order Clauses according to the sum of the Var scores") ##lavorano come categorici 2, unisci i valori, 1 follow vars, 0 follow C-specific. parser.add_argument("-considerVarsOrdering", type=int, dest="LclauseVar", default=0, help="Do not order Vars in Clauses") ##lavorano come categorici 1 linka, 0 ignora. parser.add_argument("-VnumClauses", type=float, dest="VnumClauses", default=0,help="Importance of number of clauses in which a var is involved") parser.add_argument("-VsizeClauses", type=float, dest="VsizeClauses", default=0,help="Importance of the number of vars to which this is in contact (i.e., sum of sizes of all the clauses it is involved") parser.add_argument("-VnumBinary", type=float, dest="VnumBi", default=0,help="Importance of number of binary clauses in which a var is involved") parser.add_argument("-VnumTernary", type=float, dest="VnumTri", default=0,help="Importance of number of ternary clauses in which a var is involved") parser.add_argument("-VnumMutex", type=float, dest="VnumMutex", default=0,help="Importance of mutexes relations in which a var is involved") parser.add_argument("-VtimePos", type=float, dest="VnumPos", default=0,help="Importance of number of times var appeared positive") parser.add_argument("-VtimeNeg", type=float, dest="VnumNeg",default=0, help="Importance of number of times var appeared negated") parser.add_argument("-VtimeFirstNeg", type=float, dest="VnumFNeg", default=0,help="Importance of number of times var appeared to be the first negated") parser.add_argument("-VtimeInPosClauses", type=float, dest="VnumCPos", default=0, help="Importance of number of times var appeared positive-only clauses") parser.add_argument("-VtimeInNegClauses", type=float, dest="VnumCNeg", default=0, help="Importance of number of times var appeared negated-only clauses") args = parser.parse_args() #if len(sys.argv)!=2: # print "Invalid number of arguments" # sys.exit(0) #print args.size dimacsfile=args.myFilenameVariable #dimacsfile=sys.argv[1].strip() f = open(dimacsfile, 'r') data=f.read() lines=data.split('\n') commentLine = re.compile('c.*') #Regular expression to detect comment lines statLine = re.compile('p\s*cnf\s*(\d*)\s*(\d*)') #Regular expression to detect stat line formula=[] scoreClause=[] scoreVar=[] volte_var_pos=[] volte_var_neg=[] var_sum_size_clauses=[] volte_var_binary=[] volte_var_ternary=[] volte_mutually_ex=[] #quando sono in binary entrambe negate volter_first_neg=[] volte_only_pos=[] volte_only_neg=[] for line in lines: line=line.strip() if line=="%" or not line: continue if not commentLine.match(line): stats=statLine.match(line) if stats: varCount=int(stats.group(1)) #number of unknowns volte_var_pos=[0]*(varCount+1) volte_var_neg=[0]*(varCount+1) volte_var_binary=[0]*(varCount+1) volte_var_ternary=[0]*(varCount+1) scoreVar=[0]*(varCount+1) volte_mutually_ex=[0]*(varCount+1) volte_only_pos=[0]*(varCount+1) volte_only_neg=[0]*(varCount+1) volte_first_neg=[0]*(varCount+1) var_sum_size_clauses=[0]*(varCount+1) termCount=int(stats.group(2)) #number of clauses/terms else: valueScore=0 pos=0 neg=0 allpos=0 allneg=0 numbers=line.rstrip('\n').split() literals=[] lun=len(numbers) for number in numbers: n=int(number) if(n!=0): literals.append(n) if (n > 0): pos+=1 allneg=1 volte_var_pos[n]+=1 else: neg+=1 allpos=1 volte_var_neg[-n]+=1 if lun==3: valueScore+=LARGEPOS * int(args.Cbinary) if int(numbers[0]) < 0: volte_var_binary[-int(numbers[0])]+=1 if int(numbers[1]) < 0: volte_var_binary[-int(numbers[1])]+=1 volte_mutually_ex[-int(numbers[0])]+=1 volte_mutually_ex[-int(numbers[1])]+=1 else: volte_var_binary[int(numbers[1])]+=1 else: volte_var_binary[int(numbers[0])]+=1 if allpos==0: for number in numbers: volte_only_pos[int(number)]+=1 if allneg==0: for number in numbers: volte_only_neg[-int(number)]+=1 if int(numbers[0]) < 0 and args.CfirstNeg!=0: ##scoreClause gestito qui per i first neg. valueScore+=LARGEPOS * int(args.CfirstNeg) valueScore+=pos*int(args.CposLit)+neg*int(args.CnegLit) scoreClause.append(valueScore) formula.append(literals) #print volte_var_neg ###CALCULATE SCORES. j=0 while j < len(formula): scoreClause[j]+= float(args.Csize) * len(formula[j]) if len(formula[j]) ==3: scoreClause[j]+=LARGEPOS * int(args.Cternary) if int(args.LclauseVar) != 0: for var in formula[j]: if scoreVar[abs(var)] == 0: scoreVar[abs(var)] += float(args.VnumClauses) * (volte_var_pos[abs(var)] + volte_var_neg[abs(var)]) + float(args.VnumPos) * volte_var_pos[abs(var)] + float(args.VnumNeg) * volte_var_neg[abs(var)] + float(args.VsizeClauses) * var_sum_size_clauses[abs(var)] + float(args.VnumBi) * volte_var_binary[abs(var)] + float(args.VnumTri) * volte_var_ternary[abs(var)] + float(args.VnumMutex) * volte_mutually_ex[abs(var)] + float(args.VnumFNeg) * volte_first_neg[abs(var)] + float(args.VnumCNeg) * volte_only_neg[abs(var)] + float(args.VnumCPos) * volte_only_pos[abs(var)] j+=1 #### ORDER CLAUSES if args.CorderV == 2: ##unire i valori j=0 while j < len(formula): aiuto=formula[j] for numero in aiuto: scoreClause[j]+=scoreVar[abs(numero)] j=j+1 if args.CorderV == 1: ##solo le Vars j=0 while j < len(formula): aiuto=formula[j] scoreClause[j]=0 for numero in aiuto: scoreClause[j]+=scoreVar[abs(numero)] j=j+1 ###TIME TO PRINT EVERYTHING AND ORDER VARS IN CLAUSES, IF NEEDED if sum(scoreClause) == 0: ordered=list(reversed(formula)) else: ordered=[x for _, x in sorted(zip(scoreClause,formula), key=lambda pair: pair[0])] print "p cnf "+str(varCount)+" "+str(termCount) for i in ordered[::-1]: if int(args.LclauseVar) == 0: print ' '.join(map(str, i))+" 0" else: peso=[] for j in i: peso.append(scoreVar[abs(j)]) ord_ino=[x for _, x in sorted(zip(peso,i), key=lambda pair: pair[0])] print ' '.join(map(str, ord_ino[::-1]))+" 0"