1. #lang racket
2.  
3. ;;Praca grupowa:
4. ;;Dawid Holewa
5. ;;Julita Osman
6. ;;Aleksandra Stępniewska
7.  
8. (require "props.rkt")
9. (provide falsifiable-cnf?)
10.  
11. ;Ponieważ formuła w cnf to konjunkcja klauzul
12. ;a klauzula to alternatywa literałów
13. ;to formuła w tej postaci jest tautologią
14. ;wtedy i tylko wtedy gdy
15. ;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami)
16. ;w przeciwnym razie, formulę taką da się zanegować;
17. ;zatem nasz pomysł polega na tym, aby
18. ;1)sprawdzic czy formula jest tautologia
19. ;2)jesli tak to zwracamy fałsz
20. ;3)wpp. pierwsza z klauzul, która nie jest tautologia
21. ;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf)
22. ;"przesuwamy" na początek listy reprezentującej cnf
23.  
24. ;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie
25. ;możemy skorzystać z własności alternatywy
26. ;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją
27.  
28. ;Falsifiable, która sprawdza każde wartościowania
29. ;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań,
30. ;podczas gdy
31. ;falsifiable, która opiera się na strukturze cnf
32. ;przechodzi po cnf, aż do napotkania pierwszej
33. ;mozliwej do zanegowania klauzuli
34. ;zatem w najroszym przypadku przejdziemy po całym cnf
35. ;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli
36. ;zauważmy,ze jeśli formuła jest tautologią to oszczędzamy bardzo dużo czasu nie rozpartując wszystkich wartosciowań, tylko wypisujac odrazu falsz
37.  
38. ;Ta druga jest więc efektywniejsza
39.  
40. (define (lit? f);; a lub ~a
41.   (or (var? f) ;;a
42.       (and (neg? f);;~a
43.            (var? (neg-subf f)))))
44.  
45. (define (lit-pos v)
46.   v)
47.  
48. (define (lit-neg v)
49.   (neg v))
50.  
51. (define (lit-var l) ;;a-->a      ~a-->a
52.   (if (var? l)
53.       l
54.       (neg-subf l)))
55.  
56. (define (lit-pos? l)
57.   (var? l))
58.  
59. (define (to-nnf f)
60.   (cond
61.     [(var? f)  (lit-pos f)]
62.     [(neg? f)  (to-nnf-neg (neg-subf f))]
63.     [(conj? f) (conj (to-nnf (conj-left f))
64.                      (to-nnf (conj-right f)))]
65.     [(disj? f) (disj (to-nnf (disj-left f))
66.                      (to-nnf (disj-right f)))]))
67.  
68. (define (to-nnf-neg f)
69.   (cond
70.     [(var? f)  (lit-neg f)]
71.     [(neg? f)  (to-nnf (neg-subf f))]
72.     [(conj? f) (disj (to-nnf-neg (conj-left f))
73.                      (to-nnf-neg (conj-right f)))]
74.     [(disj? f) (conj (to-nnf-neg (disj-left f))
75.                      (to-nnf-neg (disj-right f)))]))
76.  
77. (define (mk-cnf xss)
78.   (cons 'cnf xss))
79.  
80. (define (clause? f)
81.   (and (list? f)
82.        (andmap lit? f)))
83.  
84. (define (cnf? f)
85.   (and (pair? f)
86.        (eq? 'cnf (car f))
87.        (list? (cdr f))
88.        (andmap clause? (cdr f))))
89.  
90. (define (to-cnf f)
91.   (define (join xss yss)
92.     (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss)))
93.  
94.   (define (go f)
95.     (cond
96.       [(lit? f)  (list (list f))]
97.       [(conj? f) (append (go (conj-left f))
98.                          (go (conj-right f)))]
99.       [(disj? f) (join (go (disj-left f))
100.                        (go (disj-right f)))]))
101.   (mk-cnf (go f)))
102.  
103.  
104. (define (contain-both-literals?  claus)
105.   (define (aux to-check)
106.     (cond [(empty? to-check) #f]
107.           [(neg? (car to-check))
108.            (if (memq (neg-subf (car to-check)) claus)
109.                #t
110.                (aux (cdr to-check)))]
111.           [else (aux (cdr to-check))]))
112.   (aux claus))
113.  
114.  
115. ;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf
116. ;; zawiera chociaz jedną parę zmiennej i jej negacji
117. ;; zwraca liste pusta jesli cnf jest tautologia
118. ;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg)
119. (define (has-both big-set)
120.   (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek
121.     (define x-ty (list-ref big-set x))
122.     (append (list x-ty) (remove x-ty big-set)))
123.   (define (aux iter big-set)
124.   (if (= iter (length big-set))
125.       '()
126.       (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie
127.           (aux (+ iter 1) big-set)
128.           (possible-to-neg big-set iter))))
129.   (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf
130.          
131.  
132. (define (falsifiable-cnf? t)
133.   (define tt (to-cnf (to-nnf t)))
134.   (define f (has-both tt))
135.   (if (empty? f)
136.       #f
137.       (find-valuation f)))
138.            
139.  
140. (define (valuate f sigma)
141.   (define (insigma-proc lista result)
142.     (cond [(null? lista) result]
143.           [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))]))
144.   ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli:  
145.   (define insigma (insigma-proc sigma '()))
146.   (define (aux insigma otherclause sigma)
147.     (cond [(null? otherclause) sigma]
148.           [(if (memq (lit-var (car otherclause)) insigma)
149.                (aux insigma (cdr otherclause) sigma)
150.                (if(neg? (car otherclause))
151.                   (aux (append insigma (list(car otherclause)))
152.                     (cdr otherclause)
153.                     (append sigma (list(cons (lit-var(car otherclause)) 1))))
154.                   (aux (append insigma (list(car otherclause)))
155.                     (cdr otherclause)
156.                     (append sigma (list(cons (car otherclause) 0))))))]))
157.   (if (empty? f)
158.       sigma
159.       (valuate (cdr f)
160.                     (aux insigma (car f) sigma))))
161.  
162. (define (find-valuation f)
163.   (valuate f '()))
164.  
165.          
166.  
167.  
168. ;;testy:
169. (define f1
170.   (conj (neg 'p)
171.         'p))
172. (define f2
173.   (conj (disj 'p
174.               (neg 'p))
175.         'q))
176. (define f3
177.   (conj (disj 'p
178.               (neg 'p))
179.         (disj 'q
180.               (neg 'q))))
181. (define f4
182.   (conj f3
183.         'r))
184. (define f5
185.   (conj (disj 'p
186.               (neg 'p))
187.         (disj 'q
188.               (disj (neg 'q)
189.                     'r))))
190. (define f6
191.   (conj (disj 'p
192.               (neg 'p))
193.         (disj 'q
194.              'r)))
195.  
196. (define f7
197.   (conj (disj 'p
198.               (neg 'p))
199.         (disj 'q
200.               (neg 'r))))
201. (define f8
202.   (conj (disj 'q
203.               (disj 'r
204.                     's))
205.         (disj (neg 'q)
206.               (disj (neg 'r)
207.                     (neg 's)))))
208.  
209. (define f9
210.   (conj (conj-left f8)
211.         (disj 'p
212.               (neg 'p))))
213.  
214. (define f10
215.   (conj (disj 'q
216.               'r)
217.         (conj 'p
218.               (neg 'q))))
219.  
220. (define f11
221.    'p)
222.  
223. (define f12
224.   (disj 'p (neg 'p)))
225.  
226. (define f13
227.   (disj 'p
228.         (disj (neg 'p)
229.               'q)))
230.  
231. (falsifiable-cnf? f1)
232. (falsifiable-cnf? f2)
233. (falsifiable-cnf? f3)
234. (falsifiable-cnf? f4)
235. (falsifiable-cnf? f5)
236. (falsifiable-cnf? f6)
237. (falsifiable-cnf? f7)
238. (falsifiable-cnf? f8)
239. (falsifiable-cnf? f9)
240. (falsifiable-cnf? f10)
241. (falsifiable-cnf? f11)
242. (falsifiable-cnf? f12)
243. (falsifiable-cnf? f13)
244.  
245.