2 files changed, 223 insertions, 0 deletions
diff --git a/semestr-2/racket/lista5/skrr/solution.bak b/semestr-2/racket/lista5/skrr/solution.bak
new file mode 100644
index 0000000..72c7f36
--- /dev/null
+++ b/semestr-2/racket/lista5/skrr/solution.bak
@@ -0,0 +1,135 @@
+#lang racket
+
+(provide falsifiable-cnf?)
+(require "props.rkt")
+
+(define (prop? f)
+  (or (var? f)
+      (and (neg? f)
+           (prop? (neg-subf f)))
+      (and (disj? f)
+           (prop? (disj-left f))
+           (prop? (disj-right f)))
+      (and (conj? f)
+           (prop? (conj-left f))
+           (prop? (conj-right f)))))
+
+(define (lit-var f)
+  (cond [(var? f) f]
+        [(neg? f) (neg-subf f)]
+        [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
+      
+(define (free-vars f)
+  (cond [(null? f) null]
+        [(var? f) (list f)]
+        [(neg? f) (free-vars (neg-subf f))]
+        [(conj? f) (append (free-vars (conj-left f))
+                           (free-vars (conj-right f)))]
+        [(disj? f) (append (free-vars (disj-left f))
+                           (free-vars (disj-right f)))]
+        [else (error "Zła formula -- FREE-VARS" f)]))
+
+(define (gen-vals xs)
+  (if (null? xs)
+      (list null)
+      (let*
+          ((vss (gen-vals (cdr xs)))
+           (x (car xs))
+           (vst (map (λ (vs) (cons (list x true) vs)) vss))
+           (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
+        (append vst vsf))))
+
+(define (eval-formula f evaluation)
+  (cond [(var? f)
+         (let ((val (assoc f evaluation)))
+           (if (not val)
+               (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
+               (cadr val)))]
+        [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
+        [(disj? f) (or (eval-formula (disj-left f) evaluation)
+                       (eval-formula (disj-right f) evaluation))]
+        [(conj? f) (and (eval-formula (conj-left f) evaluation)
+                        (eval-formula (conj-right f) evaluation))]
+        [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
+
+(define (falsifiable-eval? f)
+  (let* ((evaluations (gen-vals (free-vars f)))
+         (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
+    (ormap false? results)))
+
+(define (nff? f)
+  (cond [(lit? f) true]
+        [(neg? f) false]
+        [(conj? f) (and (nff? (conj-left f))
+                        (nff? (conj-right f)))]
+        [(disj? f) (and (nff? (disj-left f))
+                        (nff? (disj-right f)))]
+        [else (error "Zła formuła -- NFF?" f)]))
+
+(define (convert-to-nnf f)
+  (cond [(lit? f) f]
+        [(neg? f) (convert-negation (neg-subf f))]
+        [(conj? f) (conj (convert-to-nnf (conj-left f))
+                              (convert-to-nnf (conj-right f)))]
+        [(disj? f) (disj (convert-to-nnf (disj-left f))
+                              (convert-to-nnf (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT" f)]))
+
+(define (convert-negation f)
+  (cond [(lit? f)
+         (if (var? f)
+             (neg f)
+             (neg-subf f))]
+        [(neg? f) (convert-to-nnf (neg-subf f))]
+        [(conj? f) (disj (convert-negation (conj-left f))
+                              (convert-negation (conj-right f)))]
+        [(disj? f) (conj (convert-negation (disj-left f))
+                              (convert-negation (disj-right f)))]
+        [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
+
+(define (clause? x)
+  (and (list? x)
+       (andmap lit? x)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (cnf? x)
+  (and (list? x)
+       (andmap clause? x)))
+
+(define (flatmap proc seq)
+  (foldl append null (map proc seq)))
+
+(define (convert-to-cnf f)
+  (define (convert f)
+    (cond [(lit? f) (list (list f))]
+          [(conj? f) (append (convert-to-cnf (conj-left f))
+                             (convert-to-cnf (conj-right f)))]
+          [(disj? f)
+           (let ((clause-left (convert-to-cnf (disj-left f)))
+                 (clause-right (convert-to-cnf (disj-right f))))
+             (flatmap (λ (clause)
+                        (map (λ (clause2)
+                               (append clause2 clause)) clause-left))
+                      clause-right))]))
+  (convert (convert-to-nnf f)))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (convert-to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
+\ No newline at end of file
diff --git a/semestr-2/racket/lista5/skrr/solution.rkt b/semestr-2/racket/lista5/skrr/solution.rkt
new file mode 100644
index 0000000..e8efbc9
--- /dev/null
+++ b/semestr-2/racket/lista5/skrr/solution.rkt
@@ -0,0 +1,88 @@
+#lang racket
+
+(require "props.rkt")
+(provide falsifiable-cnf?)
+
+(define (lit? f)
+  (or (var? f)
+      (and (neg? f)
+           (var? (neg-subf f)))))
+
+(define (lit-pos v)
+  v)
+
+(define (lit-neg v)
+  (neg v))
+
+(define (lit-var l)
+  (if (var? l)
+      l
+      (neg-subf l)))
+
+(define (lit-pos? l)
+  (var? l))
+
+(define (to-nnf f)
+  (cond
+   [(var? f)  (lit-pos f)]
+   [(neg? f)  (to-nnf-neg (neg-subf f))]
+   [(conj? f) (conj (to-nnf (conj-left f))
+                    (to-nnf (conj-right f)))]
+   [(disj? f) (disj (to-nnf (disj-left f))
+                    (to-nnf (disj-right f)))]))
+
+(define (to-nnf-neg f)
+  (cond
+   [(var? f)  (lit-neg f)]
+   [(neg? f)  (to-nnf (neg-subf f))]
+   [(conj? f) (disj (to-nnf-neg (conj-left f))
+                    (to-nnf-neg (conj-right f)))]
+   [(disj? f) (conj (to-nnf-neg (disj-left f))
+                    (to-nnf-neg (disj-right f)))]))
+
+(define (mk-cnf xss)
+  (cons 'cnf xss))
+
+(define (clause? f)
+  (and (list? f)
+       (andmap lit? f)))
+
+(define (cnf? f)
+  (and (pair? f)
+       (eq? 'cnf (car f))
+       (list? (cdr f))
+       (andmap clause? (cdr f))))
+
+(define (to-cnf f)
+  (define (join xss yss)
+    (apply append (map (lambda (xs) (map (lambda (ys) (append xs ys)) yss)) xss)))
+  (define (go f)
+    (cond
+     [(lit? f)  (list (list f))]
+     [(conj? f) (append (go (conj-left f))
+                        (go (conj-right f)))]
+     [(disj? f) (join (go (disj-left f))
+                      (go (disj-right f)))]))
+  (mk-cnf (go f)))
+
+(define (clause-empty? x)
+  (and (clause? x)
+       (null? x)))
+
+(define (falsifiable-clause? clause)
+  (cond [(clause-empty? clause) true]
+        [(lit? (findf (λ (l) (equal?
+                              l
+                              (to-nnf (neg (car clause)))))
+                              clause)) false]
+        [else (falsifiable-clause? (cdr clause))]))
+
+(define (falsifiable-cnf? f)
+  (define (neg-value lit)
+    (if (var? lit)
+        (list lit false)
+        (list (neg-subf lit) true)))
+  (ormap (λ (clause) (if (falsifiable-clause? clause)
+                         (map neg-value clause)
+                         false))
+         (convert-to-cnf f)))
+\ No newline at end of file