• API
• FAQ
• Tools
• Trends
• Archive
daily pastebin goal
43%
SHARE
TWEET

# Untitled

a guest Mar 20th, 2017 68 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.
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.