diff options
Diffstat (limited to 'Semestr 2/racket/lista5')
21 files changed, 1104 insertions, 0 deletions
diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep new file mode 100644 index 0000000..6e0cfbb --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.dep @@ -0,0 +1 @@ +("7.6" racket ("f0a57e86828cdab35eaad454d5deb80353172518" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo Binary files differnew file mode 100644 index 0000000..748fec9 --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/prop_rkt.zo diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep new file mode 100644 index 0000000..0926afc --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.dep @@ -0,0 +1 @@ +("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo Binary files differnew file mode 100644 index 0000000..eccc7f7 --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/props_rkt.zo diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep new file mode 100644 index 0000000..9810b4c --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.dep @@ -0,0 +1 @@ +("7.6" racket ("ae3a6974cdd4582f480927d9968aad2f495b7fc4" . "33b0c09c14dce6a2115d810ac3d0f25a9dce3205") #"C:\\Users\\franc\\Documents\\lista5\\props.rkt" (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo Binary files differnew file mode 100644 index 0000000..ca1ab20 --- /dev/null +++ b/Semestr 2/racket/lista5/compiled/drracket/errortrace/solution_rkt.zo diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep new file mode 100644 index 0000000..0926afc --- /dev/null +++ b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep @@ -0,0 +1 @@ +("7.6" racket ("e0347fa7e89f59bc97c197db02b440f666222428" . "8314027ed4c1c6fd9c412af77103e94790e59dd2") (collects #"errortrace" #"errortrace-key.rkt") (collects #"racket" #"main.rkt") (collects #"racket" #"runtime-config.rkt")) diff --git a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo Binary files differnew file mode 100644 index 0000000..eccc7f7 --- /dev/null +++ b/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo diff --git a/Semestr 2/racket/lista5/julita/props.rkt b/Semestr 2/racket/lista5/julita/props.rkt new file mode 100644 index 0000000..204b108 --- /dev/null +++ b/Semestr 2/racket/lista5/julita/props.rkt @@ -0,0 +1,52 @@ +#lang racket + +(provide conj conj-left conj-right conj? + disj disj-left disj-right disj? + neg neg-subf neg? + var?) + + +(define (conj p q) + (list 'conj p q)) + +(define (conj-left f) + (second f)) + +(define (conj-right f) + (third f)) + +(define (conj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'conj (car t)))) + + +(define (disj p q) + (list 'disj p q)) + +(define (disj-left f) + (second f)) + +(define (disj-right f) + (third f)) + +(define (disj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'disj (car t)))) + + +(define (neg x) + (list 'neg x)) + +(define (neg-subf x) + (second x)) + +(define (neg? t) + (and (list? t) + (= 2 (length t)) + (eq? 'neg (car t)))) + + +(define (var? t) + (symbol? t)) diff --git a/Semestr 2/racket/lista5/julita/solution.bak b/Semestr 2/racket/lista5/julita/solution.bak new file mode 100644 index 0000000..b3dda94 --- /dev/null +++ b/Semestr 2/racket/lista5/julita/solution.bak @@ -0,0 +1,164 @@ +#lang racket + +;;Praca grupowa: +;;Dawid Holewa +;;Julita Osman +;;Aleksandra Stępniewska + +(require "props.rkt") +(provide falsifiable-cnf?) + +;Ponieważ formuła w cnf to konjunkcja klauzul +;a klauzula to alternatywa literałów +;to formuła w tej postaci jest tautologią +;wtedy i tylko wtedy gdy +;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami) +;w przeciwnym razie, formulę taką da się zanegować; +;zatem nasz pomysł polega na tym, aby +;1)sprawdzic czy formula jest tautologia +;2)jesli tak to zwracamy fałsz +;3)wpp. pierwsza z klauzul, która nie jest tautologia +;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf) +;"przesuwamy" na początek listy reprezentującej cnf + +;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie +;możemy skorzystać z własności alternatywy +;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją + +;Falsifiable, która sprawdza każde wartościowania +;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań, +;podczas gdy +;falsifiable, która opiera się na strukturze cnf +;przechodzi po cnf, aż do napotkania pierwszej +;mozliwej do zanegowania klauzuli +;zatem w najroszym przypadku przejdziemy po całym cnf +;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli +;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 + +;Ta druga jest więc efektywniejsza + +(define (lit? f);; a lub ~a + (or (var? f) ;;a + (and (neg? f);;~a + (var? (neg-subf f))))) + +(define (lit-pos v) + v) + +(define (lit-neg v) + (neg v)) + +(define (lit-var l) ;;a-->a ~a-->a + (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 (contain-both-literals? claus) + (define (aux to-check) + (cond [(empty? to-check) #f] + [(neg? (car to-check)) + (if (memq (neg-subf (car to-check)) claus) + #t + (aux (cdr to-check)))] + [else (aux (cdr to-check))])) + (aux claus)) + + +;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf +;; zawiera chociaz jedną parę zmiennej i jej negacji +;; zwraca liste pusta jesli cnf jest tautologia +;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg) +(define (has-both big-set) + (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek + (define x-ty (list-ref big-set x)) + (append (list x-ty) (remove x-ty big-set))) + (define (aux iter big-set) + (if (= iter (length big-set)) + '() + (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie + (aux (+ iter 1) big-set) + (possible-to-neg big-set iter)))) + (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf + + +(define (falsifiable-cnf? t) + (define tt (to-cnf (to-nnf t))) + (define f (has-both tt)) + (if (empty? f) + #f + (find-valuation f))) + + +(define (valuate f sigma) + (define (insigma-proc lista result) + (cond [(null? lista) result] + [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))])) + ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli: + (define insigma (insigma-proc sigma '())) + (define (aux insigma otherclause sigma) + (cond [(null? otherclause) sigma] + [(if (memq (lit-var (car otherclause)) insigma) + (aux insigma (cdr otherclause) sigma) + (if(neg? (car otherclause)) + (aux (append insigma (list(car otherclause))) + (cdr otherclause) + (append sigma (list(list (lit-var(car otherclause)) 1)))) + (aux (append insigma (list(car otherclause))) + (cdr otherclause) + (append sigma (list(list (car otherclause) 0))))))])) + (if (empty? f) + sigma + (valuate (cdr f) + (aux insigma (car f) sigma)))) + +(define (find-valuation f) + (valuate f '())) + diff --git a/Semestr 2/racket/lista5/julita/solution.rkt b/Semestr 2/racket/lista5/julita/solution.rkt new file mode 100644 index 0000000..da87bf9 --- /dev/null +++ b/Semestr 2/racket/lista5/julita/solution.rkt @@ -0,0 +1,164 @@ +#lang racket + +;;Praca grupowa: +;;Dawid Holewa +;;Julita Osman +;;Aleksandra Stępniewska + +(require "props.rkt") +(provide falsifiable-cnf?) + +;Ponieważ formuła w cnf to konjunkcja klauzul +;a klauzula to alternatywa literałów +;to formuła w tej postaci jest tautologią +;wtedy i tylko wtedy gdy +;wszystkie klauzule w niej występujace sa zawsze prawdziwe (też są tautologiami) +;w przeciwnym razie, formulę taką da się zanegować; +;zatem nasz pomysł polega na tym, aby +;1)sprawdzic czy formula jest tautologia +;2)jesli tak to zwracamy fałsz +;3)wpp. pierwsza z klauzul, która nie jest tautologia +;(zatem jest mozliwa do zanegowania i jednocześnie neguje cała formułe w cnf) +;"przesuwamy" na początek listy reprezentującej cnf + +;dodatkowo to czy klauzula jest tautologią nie musimy sprawdzać wykonując wartościowanie +;możemy skorzystać z własności alternatywy +;klauzula bedzię zawsze pawdziwa tylko jeśli conajmniej jedna ze zmiennych występuje jednoczesnie ze swoją negacją + +;Falsifiable, która sprawdza każde wartościowania +;sprawdza 2^(ilosc zmiennych w całym wyrażeniu) wartosciowań, +;podczas gdy +;falsifiable, która opiera się na strukturze cnf +;przechodzi po cnf, aż do napotkania pierwszej +;mozliwej do zanegowania klauzuli +;zatem w najroszym przypadku przejdziemy po całym cnf +;ale zawsze wartosciowania negujacego formule szukamy tylko dla jedenej klauzuli +;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 + +;Ta druga jest więc efektywniejsza + +(define (lit? f);; a lub ~a + (or (var? f) ;;a + (and (neg? f);;~a + (var? (neg-subf f))))) + +(define (lit-pos v) + v) + +(define (lit-neg v) + (neg v)) + +(define (lit-var l) ;;a-->a ~a-->a + (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 (contain-both-literals? claus) + (define (aux to-check) + (cond [(empty? to-check) #f] + [(neg? (car to-check)) + (if (memq (neg-subf (car to-check)) claus) + #t + (aux (cdr to-check)))] + [else (aux (cdr to-check))])) + (aux claus)) + + +;; sprawdza czy ktorakolwiek z klauzul z listy reprezentujacej cnf +;; zawiera chociaz jedną parę zmiennej i jej negacji +;; zwraca liste pusta jesli cnf jest tautologia +;; zwraca liste z pierwsza klauzule nie bedaca tautologia "przesunieta" na poczatek (possible-to-neg) +(define (has-both big-set) + (define (possible-to-neg big-set x) ;;przesuwa x-ty element listy big-set na poczatek + (define x-ty (list-ref big-set x)) + (append (list x-ty) (remove x-ty big-set))) + (define (aux iter big-set) + (if (= iter (length big-set)) + '() + (if (contain-both-literals? (list-ref big-set iter)) ;;sprawdzamy czy iter klauzula cnf ma wystapienie a i ~a jednoczesnie + (aux (+ iter 1) big-set) + (possible-to-neg big-set iter)))) + (aux 0 (cdr big-set))) ;;(cdr big-set) bo to cnf czyli pierwszy element listy to edykieta 'cnf + + +(define (falsifiable-cnf? t) + (define tt (to-cnf (to-nnf t))) + (define f (has-both tt)) + (if (empty? f) + #f + (find-valuation f))) + + +(define (valuate f sigma) + (define (insigma-proc lista result) + (cond [(null? lista) result] + [(insigma-proc (cdr lista) (append result (list (lit-var(caar lista)))))])) + ;; insigma ---> lista zmiennych z wartosciowania pierwszej klauzuli: + (define insigma (insigma-proc sigma '())) + (define (aux insigma otherclause sigma) + (cond [(null? otherclause) sigma] + [(if (memq (lit-var (car otherclause)) insigma) + (aux insigma (cdr otherclause) sigma) + (if(neg? (car otherclause)) + (aux (append insigma (list(car otherclause))) + (cdr otherclause) + (append sigma (list(list (lit-var(car otherclause)) true)))) + (aux (append insigma (list(car otherclause))) + (cdr otherclause) + (append sigma (list(list (car otherclause) false))))))])) + (if (empty? f) + sigma + (valuate (cdr f) + (aux insigma (car f) sigma)))) + +(define (find-valuation f) + (valuate f '())) + diff --git a/Semestr 2/racket/lista5/prop.rkt b/Semestr 2/racket/lista5/prop.rkt new file mode 100644 index 0000000..6f1f7b4 --- /dev/null +++ b/Semestr 2/racket/lista5/prop.rkt @@ -0,0 +1 @@ +#lang racket diff --git a/Semestr 2/racket/lista5/props.bak b/Semestr 2/racket/lista5/props.bak new file mode 100644 index 0000000..1a5659a --- /dev/null +++ b/Semestr 2/racket/lista5/props.bak @@ -0,0 +1,71 @@ +#lang racket + +(provide var? + neg? + conj? + disj? + conj + disj + neg + conj-left + conj-right + disj-right + disj-left + neg-subf) +; (require "solution.rkt") + +(define (var? t) (symbol? t)) + +(define (neg? t) + (and (list? t) + (= 2 (length t)) + (eq? 'neg (car t)))) + +(define (conj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'conj (car t)))) + +(define (disj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'disj (car t)))) + +(define (lit? t) + (or (var? t) + (and (neg? t) + (var? (neg-subf t))))) + +(define (conj left right) + (list 'conj left right)) + +(define (disj left right) + (list 'disj left right)) + +(define (neg f) + (list 'neg f)) + +(define (conj-left f) + (if (conj? f) + (cadr f) + (error "Złe dane ze znacznikiem -- CONJ-LEFT" f))) + +(define (conj-right f) + (if (conj? f) + (caddr f) + (error "Złe dane ze znacznikiem -- CONJ-RIGHT" f))) + +(define (disj-left f) + (if (disj? f) + (cadr f) + (error "Złe dane ze znacznikiem -- DISJ-LEFT" f))) + +(define (disj-right f) + (if (disj? f) + (caddr f) + (error "Złe dane ze znacznikiem -- DISJ-RIGHT" f))) + +(define (neg-subf f) + (if (neg? f) + (cadr f) + (error "Złe dane ze znacznikiem -- NEG-FORM" f))) diff --git a/Semestr 2/racket/lista5/props.rkt b/Semestr 2/racket/lista5/props.rkt new file mode 100644 index 0000000..204b108 --- /dev/null +++ b/Semestr 2/racket/lista5/props.rkt @@ -0,0 +1,52 @@ +#lang racket + +(provide conj conj-left conj-right conj? + disj disj-left disj-right disj? + neg neg-subf neg? + var?) + + +(define (conj p q) + (list 'conj p q)) + +(define (conj-left f) + (second f)) + +(define (conj-right f) + (third f)) + +(define (conj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'conj (car t)))) + + +(define (disj p q) + (list 'disj p q)) + +(define (disj-left f) + (second f)) + +(define (disj-right f) + (third f)) + +(define (disj? t) + (and (list? t) + (= 3 (length t)) + (eq? 'disj (car t)))) + + +(define (neg x) + (list 'neg x)) + +(define (neg-subf x) + (second x)) + +(define (neg? t) + (and (list? t) + (= 2 (length t)) + (eq? 'neg (car t)))) + + +(define (var? t) + (symbol? t)) 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 diff --git a/Semestr 2/racket/lista5/sol2.rkt b/Semestr 2/racket/lista5/sol2.rkt new file mode 100644 index 0000000..d037472 --- /dev/null +++ b/Semestr 2/racket/lista5/sol2.rkt @@ -0,0 +1,90 @@ +#lang racket +(provide falsifiable-cnf?) (require "props.rkt") + + +(define (falsifiable-cnf? p) + ;literał + (define (lit? p) + (or (var? p) + (and (neg? p) (var? (neg-subf p))) + )) + + (define (lit-pos? p) + (if (lit? p) + (var? p) + (error "not a literal" p) + )) + + (define (lit-var p) + (cond + [(not (lit? p)) (error "not a literal" p)] + [(lit-pos? p) p] + [else (neg-subf p)] + )) + + (define (contr p) + (if (lit? p) + (if (neg? p) (neg-subf p) (neg p)) + (error "not a literal" p) + )) + + ;konwertowanie + (define (convert-to-cnf p) + (define (convert-to-nnf p) + (cond + [(lit? p) p] + [(and (neg? p) (conj? (neg-subf p))) + (let ((A (neg-subf p))) + (disj (convert-to-nnf (neg (conj-left A))) (convert-to-nnf (neg (conj-right A)))))] + [(and (neg? p) (disj? (neg-subf p))) + (let ((A (neg-subf p))) + (conj (convert-to-nnf (neg (disj-left A))) (convert-to-nnf (neg (disj-right A)))))] + [(and (neg? p) (neg? (neg-subf p))) (convert-to-nnf (neg-subf (neg-subf p)))] + [(conj? p) (conj (convert-to-nnf (conj-right p)) (convert-to-nnf (conj-left p)))] + [(disj? p) (disj (convert-to-nnf (disj-right p)) (convert-to-nnf (disj-left p)))] + [else (error "not a proposition" p)])) + + (define (flatmap proc seq) + (foldr append null (map proc seq))) + + (define (merge a b) + (flatmap (lambda (c) (map (lambda (c2) (append c c2)) b)) a)) + + (define (convert p) + (cond + [(lit? p) (list (list p))] + [(conj? p) (append (convert (conj-left p)) (convert (conj-right p)))] + [(disj? p) (let* ((L (convert (disj-left p))) (R (convert (disj-right p)))) + (merge L R))] + [else (error "it should never be here" p)] + )) + + (map (lambda (c) (remove-duplicates c)) (convert (convert-to-nnf p)))) + + ;prawdziwa funkcja + (define cnf (convert-to-cnf p)) + + (define (falsifiable-clause? c) + (cond + [(null? c) #t] + [(eq? #f (member (contr (car c)) c)) (falsifiable-clause? (cdr c))] + [else #f] + )) + + (define (falsified-clause c) + (if (null? c) + null + (cons (list (lit-var (car c)) (not (lit-pos? (car c)))) (falsified-clause (cdr c))) + )) + + (define (falsified-val p) + (cond + [(null? p) false] + [(falsifiable-clause? (car p)) (falsified-clause (car p))] + [else (falsified-val (cdr p))] + ) + ) + (falsified-val cnf)) + + +;złożoność wykładnicza tak jak falsible-eval ale często w praktyce szybsza jak nie ma za dużo alternatyw.
\ No newline at end of file diff --git a/Semestr 2/racket/lista5/solution.bak b/Semestr 2/racket/lista5/solution.bak new file mode 100644 index 0000000..72c7f36 --- /dev/null +++ b/Semestr 2/racket/lista5/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/solution.rkt b/Semestr 2/racket/lista5/solution.rkt new file mode 100644 index 0000000..67964d8 --- /dev/null +++ b/Semestr 2/racket/lista5/solution.rkt @@ -0,0 +1,140 @@ +#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? t) + (or (var? t) + (and (neg? t) + (var? (neg-subf t))))) + +(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))])) + (map (lambda (clause) (remove-duplicates clause)) (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/xd.bak b/Semestr 2/racket/lista5/xd.bak new file mode 100644 index 0000000..d814e10 --- /dev/null +++ b/Semestr 2/racket/lista5/xd.bak @@ -0,0 +1,4 @@ +#lang racket + +(require "solution.rkt") + diff --git a/Semestr 2/racket/lista5/xd.rkt b/Semestr 2/racket/lista5/xd.rkt new file mode 100644 index 0000000..64ce78c --- /dev/null +++ b/Semestr 2/racket/lista5/xd.rkt @@ -0,0 +1,4 @@ +#lang racket + +(require "solution.rkt") +(require "props.rkt") |