aboutsummaryrefslogtreecommitdiff
path: root/Semestr 2/racket/lista5/julita
diff options
context:
space:
mode:
authorFranciszek Malinka <franciszek.malinka@gmail.com>2021-10-05 21:49:54 +0200
committerFranciszek Malinka <franciszek.malinka@gmail.com>2021-10-05 21:49:54 +0200
commitc5fcf7179a83ef65c86c6a4a390029149e518649 (patch)
treed29ffc5b86a0d257453cedcf87d91a13d8bf3b0d /Semestr 2/racket/lista5/julita
parentf8a88b6a4aba1f66d04711a9330eaba49a50c463 (diff)
Duzy commit ze smieciami
Diffstat (limited to 'Semestr 2/racket/lista5/julita')
-rw-r--r--Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep1
-rw-r--r--Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zobin3273 -> 0 bytes
-rw-r--r--Semestr 2/racket/lista5/julita/props.rkt52
-rw-r--r--Semestr 2/racket/lista5/julita/solution.bak164
-rw-r--r--Semestr 2/racket/lista5/julita/solution.rkt164
5 files changed, 0 insertions, 381 deletions
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
deleted file mode 100644
index 0926afc..0000000
--- a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.dep
+++ /dev/null
@@ -1 +0,0 @@
-("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
deleted file mode 100644
index eccc7f7..0000000
--- a/Semestr 2/racket/lista5/julita/compiled/drracket/errortrace/props_rkt.zo
+++ /dev/null
Binary files differ
diff --git a/Semestr 2/racket/lista5/julita/props.rkt b/Semestr 2/racket/lista5/julita/props.rkt
deleted file mode 100644
index 204b108..0000000
--- a/Semestr 2/racket/lista5/julita/props.rkt
+++ /dev/null
@@ -1,52 +0,0 @@
-#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
deleted file mode 100644
index b3dda94..0000000
--- a/Semestr 2/racket/lista5/julita/solution.bak
+++ /dev/null
@@ -1,164 +0,0 @@
-#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
deleted file mode 100644
index da87bf9..0000000
--- a/Semestr 2/racket/lista5/julita/solution.rkt
+++ /dev/null
@@ -1,164 +0,0 @@
-#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 '()))
-