SHARE
TWEET

Untitled

a guest Mar 20th, 2017 66 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. import os
  2. import sys
  3. sys.path[0:0] = [os.path.join(sys.path[0], '../examples/sat')]
  4. import sat
  5.  
  6. Howard = 0
  7. George = 1
  8. Virginia = 2
  9. Dorothy = 3
  10. mena = ['Howard', 'George', 'Virginia', 'Dorothy']
  11. ludia = [Howard, George, Virginia, Dorothy]
  12. zeny = [Virginia,Dorothy]
  13. muzi = [Howard, George]
  14.  
  15. def O(x): # otec
  16.     return 0+x+1
  17.  
  18. def M(x): # matka
  19.     return 4+x+1
  20.  
  21. def S(x): # syn
  22.     return 8+x+1
  23.  
  24. def D(x): # dcera
  25.     return 12+x+1
  26.  
  27. def pp(x, y):
  28.     return 16+4*x+y+1
  29.  
  30. def st(x, y):
  31.     return 32+4*x+y+1
  32.  
  33. def ml(x, y):
  34.     return 48+4*x+y+1
  35.  
  36. def hadanka():
  37.     solver = sat.SatSolver()
  38.     w = sat.DimacsWriter("vstup.txt")
  39.  
  40.     for x in ludia:
  41.         for y in ludia:
  42.             w.writeClause([-pp(x,y), -O(x), -M(x)])
  43.             w.writeImpl(pp(x, y), pp(y, x))
  44.  
  45. ##    zeny nie su otec/syn a muzi nie su matka/dcera
  46.     for mnozina, rola, rola2 in [(Muzi, M, D), (Zeny, O, S)]:
  47.         for x in mnozina:
  48.             w.writeClause([-rola(x)])
  49.             w.writeClause([-rola2(x)])
  50.  
  51.     for rola in [O, S]:
  52. ##        aspon jeden otec/syn | (OG v OH) | (SG v SH)
  53.         w.writeClause([rola(Howard), rola(George)])
  54. ##        nie dvaja otcovia/synovia | -(OG ^ OH) | -(SG ^ SH)
  55.         w.writeClause([-rola(Howard), -rola(George)])
  56.  
  57. ##    muz nemoze byt oboje naraz | Ak je otec, nemoze byt syn
  58.     for muz in Muzi:
  59.         w.writeClause([-O(muz), -S(muz)])
  60.  
  61. ##    w.writeClause([-O(Howard), -O(George)])
  62.  
  63.     for rola in [M, D]:
  64. ##        aspon jedna matka/dcera | (MV v MD) | (DV v DD)
  65.         w.writeClause([rola(Virginia), rola(Dorothy)])
  66. ##        nie dve matky/dcery | -(MV ^ MD) | -(DV ^ DD)
  67.         w.writeClause([-rola(Virginia), -rola(Dorothy)])
  68.  
  69. ##    zena nemoze byt oboje naraz | Ak je matka, nemoze byt dcera
  70.     for zena in Zeny:
  71.         w.writeClause([-M(zena), -D(zena)])
  72.  
  73.     for z in zeny:
  74.         w.writeClause([-O(z), -S(z)])
  75.        
  76.     for m in muzi:
  77.         w.writeClause([-M(m), -D(m)])
  78.  
  79. ##    tvrdenia
  80.     tvr1 = pp(George, Dorothy)
  81.     tvr2 = st(Howard, George)
  82.     tvr3 = ml(Virginia, Howard)
  83.     tvr4 = st(Virginia, Dorothy)
  84.     tvr  = [tvr1, tvr2, tvr3, tvr4]
  85.  
  86. ##    prave dva trdenia su pravdive
  87.     for i in range(4):
  88.         for j in range(4):
  89.             for k in range(4):
  90.                 if i != j and j != k and i != k:
  91.                     w.writeClause([-tvr[i], -tvr[j], -tvr[k]])
  92.                     w.writeClause([tvr[i], tvr[j], tvr[k]])
  93.  
  94.     for x in ludia:
  95.         for y in ludia:
  96.             if x != y:
  97.                 w.writeClause([st(x, y), -st(y, x)])
  98.                 w.writeClause([st(x, y), -ml(x, y)])
  99.                 w.writeClause([-st(x, y), -O(y), -S(x)])
  100.                 w.writeClause([-st(x, y), -O(y), -D(x)])
  101.                 w.writeClause([-st(x, y), -M(y), -S(x)])
  102.                 w.writeClause([-st(x, y), -M(y), -D(x)])
  103.                 w.writeClause([-ml(x, y), -S(y), -O(x)])
  104.                 w.writeClause([-ml(x, y), -D(y), -O(x)])
  105.                 w.writeClause([-ml(x, y), -S(y), -M(x)])
  106.                 w.writeClause([-ml(x, y), -D(y), -M(x)])
  107.                
  108.                
  109.  
  110.    
  111.     w.close()
  112.     ok, sol = solver.solve(w, 'vystup.txt')
  113.  
  114.     if ok:
  115.         for i in sol:
  116.             i -= 1
  117.             if 0 <= i <= 3:
  118.                 print("Otec: ", mena[i % 4])
  119.             elif 4 <= i <= 7:
  120.                 print("Matka: ", mena[i % 4])
  121.             elif 8 <= i <= 11:
  122.                 print("Syn: ", mena[i % 4])
  123.             elif 12 <= i <= 15:
  124.                 print("Dcera: ", mena[i % 4])
  125.     else:
  126.         print("Nema riesenie")
  127.  
  128. hadanka()
RAW Paste Data
Top