blob: e8efbc9173a16e6b6fa6f1776a2493472bca560b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
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)))
|
