1 files changed, 88 insertions, 0 deletions
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