nzm

n-vivace-satreach-cyber/.gitignore

 *cnf
 *dat
+__pycache__/
+__pycache__/*

n-vivace-satreach-cyber/c-ECApaths.py

 import os, sys
 import subprocess
 import re
+import yNaming as naming
 
-ECA=110
+
+ECA=22
 TSTEPS=70
-x, y = "0101010011010011011101", "1011101101110110111001"
+x, y = "010101001111010011011101", "101110110001110110111001"
 
 EXCEPTIONMINISAT=2560
 
@@ -16,29 +18,36 @@ def runcmd(cmd):
     
 
 def run():
-    basename="ECA%d-%s-%s"%(ECA,x,y)
+    hashx,hashy=naming.shorthash(x),naming.shorthash(y) # configs : using short hash for
+    basename="ECA%d-%s-%s"%(ECA,hashx,hashy)
     cmd1="python3 b-satkubernetes.py %d %d %s %s > %s.dat"%(ECA, TSTEPS, x, y, basename)
     cmd2="python3 x2-convertToSat.py %s.dat "%basename
-    cmd3="minisat %s.cnf Zsol-%s.cnf"%(basename,basename)
+    cmd3="minisat %s.cnf %s-sol.cnf"%(basename,basename)
     ncells=len(x)+2
-    cmd4="python3 w-prnCNFsolution.py %d Zsol-%s.cnf"%(ncells, basename)
+    cmd4="python3 w-prnCNFsolution.py %d %s-sol.cnf"%(ncells, basename)
     cmdseq=[cmd1,cmd2,cmd3,cmd4]
-    subprocess.run(cmd1.split())
-    subprocess.run(cmd2.split())
+    for cmd in cmdseq:
+        print(cmd)
+    subprocess.getoutput(cmd1)
+    subprocess.getoutput(cmd2)
     #------------------------------
-    result = subprocess.getoutput(cmd3)
+    res3 = subprocess.getoutput(cmd3)
     #------------------------------
-    subprocess.run(cmd4.split())
+    subprocess.getoutput(cmd4)
+    
+    itimeCPU=res3.index("CPU time")
+    part= res3[itimeCPU+20:itimeCPU+35].strip()
     
-    itimeCPU=result.index("CPU time")
-    part= result[itimeCPU+20:itimeCPU+35].strip()
-    #print("part:[%s]"%part)
+    indexsol=res3.index("SATIS")
+    part2=res3[indexsol-2:].strip()
+    print("part2:[%s]"%part2)
+    satres=re.search("^U?N?SAT",part2)
+    print("res:",satres.group(0))
     tim=re.search("\d[.]?\d+", part)
     if tim:
         print("satsolver CPU time:%s"%tim.group(0))
     else:
         print("time could not be extracted")
     
-
 run()
 

n-vivace-satreach-cyber/yNaming.py

-########### Naming scheme ##################
+import hashlib
+
+############ HASH ######
+
+HASHLEN=6
+CHARTABLE = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz";
+L=len(CHARTABLE)
+
+
+def shorthash(strconfig):
+    """ produces a short hash of len HASHLEN """
+    hex=hashlib.sha1(strconfig.encode('utf-8')).hexdigest() # calc hash in hexadecimal
+    inthash=int(hex, 16) #convert to int
+    shorthash="" # projection 
+    for i in range(HASHLEN):
+        chrnew=CHARTABLE[inthash%L]
+        shorthash+=chrnew
+        inthash//=L 
+    return shorthash
+
+
+########### Naming scheme for SAT variables ##################
 
 def letterpos(pos):
     """ from int <26 to letter with the alphabet [a-z] s"""
@@ -39,3 +60,12 @@ def signedName(bit, t, i):
 def invertSignedName(bit, t, i):
     return invertedSignedVar(bit,vnamet(t,i) )
 
+############# TESTS
+
+TSTHASH=['0101','0100','010101010','00001101010','1010101010101011110101010']
+
+def testhash():
+     for strcode in TSTHASH:
+        print("%10s -> %s"%(strcode, shorthash(strcode)))
+
+#testhash()
\ No newline at end of file