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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
; Copyright (C) 2016, Regents of the University of Texas
; Marijn Heule, Warren A. Hunt, Jr., and Matt Kaufmann
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; See soundness.lisp. Here we prove a key lemma in support of that book.
(in-package "LRAT")
(include-book "truth-monotone")
(include-book "unit-propagation-monotone")
(include-book "unit-propagation-implies-unsat")
(defthm not-conflicting-literalsp-implies-negate-is-not-member
(implies (and (member lit a)
(not (conflicting-literalsp a))
(literal-listp a))
(not (member (negate lit) a))))
(defthm not-conflicting-literalsp-implies-negate-is-not-member-subset
(implies (and (subsetp a1 a2)
(member lit a2)
(not (conflicting-literalsp a2))
(literal-listp a2))
(not (member (negate lit) a1))))
(defthm subsetp-union-equal-2
(implies (subsetp x z)
(subsetp x (union$ y z))))
(defthm not-conflicting-literalsp-subsetp
(implies (and (subsetp a1 a2)
(literal-listp a2)
(not (conflicting-literalsp a2)))
(not (conflicting-literalsp a1))))
(defthm union-preserves-subsetp-2
(implies (subsetp y z)
(subsetp (union$ x y)
(union$ x z))))
(defthm conflicting-literalsp-preserved-by-union-equal-cons-2
(implies (and (not (conflicting-literalsp (union$ a1 a2)))
(literalp lit)
(not (member (negate lit) a1))
(not (member (negate lit) a2)))
(not (conflicting-literalsp (union$ a1 (cons lit a2))))))
(defthm conflicting-literalsp-union-when-member
(implies (and (literal-listp a1)
(not (conflicting-literalsp a1))
(literal-listp a2)
(not (conflicting-literalsp a2))
(member lit a1))
(iff (conflicting-literalsp
(union-equal a1 (cons lit a2)))
(conflicting-literalsp
(union-equal a1 a2))))
:hints (("Goal"
:induct (union-equal a1 a2)
:restrict
((not-conflicting-literalsp-implies-negate-is-not-member-subset
((a2 (union-equal (cdr a1) (cons (car a1) a2)))))
(not-conflicting-literalsp-subsetp
((a2 (union-equal (cdr a1) (cons (car a1) a2)))))))))
; Start proof of not-conflicting-literalsp-union
(encapsulate
()
(local
(defthm evaluate-clause-union-equal-cons-2
(implies (and (not (member-equal lit clause))
(equal (evaluate-clause clause
(union-equal assignment (cons lit y)))
t))
(equal (evaluate-clause clause
(union-equal assignment y))
t))))
(local
(defthm not-conflicting-literalsp-union-lemma
(implies (and (literal-listp clause)
(literal-listp y) ; needed?
(not (conflicting-literalsp clause))
(not (conflicting-literalsp (union-equal assignment y)))
(not (equal (evaluate-clause clause (union-equal assignment y))
t)))
(not (conflicting-literalsp
(union-equal assignment
(negate-clause-or-assignment-rec clause y)))))))
(local
(defthm evaluate-clause-union-equal-nil
(equal (evaluate-clause clause (union-equal x nil))
(evaluate-clause clause x))))
(local
(defthm conflicting-literalsp-union-equal-nil
(iff (conflicting-literalsp (union-equal x nil))
(conflicting-literalsp x))))
(defthm not-conflicting-literalsp-union
(implies (and (literal-listp clause)
(not (conflicting-literalsp clause))
(not (conflicting-literalsp assignment))
(not (equal (evaluate-clause clause assignment)
t)))
(not (conflicting-literalsp
(union-equal assignment
(negate-clause-or-assignment clause)))))
:hints (("Goal" :in-theory (enable negate-clause-or-assignment)))))
(defthm clause-or-assignment-p-union
(implies (and (clause-or-assignment-p clause)
(clause-or-assignment-p assignment)
(not (equal (evaluate-clause clause assignment)
t)))
(clause-or-assignment-p
(union$ assignment
(negate-clause-or-assignment clause))))
:hints (("Goal" :in-theory (enable clause-or-assignment-p))))
(defthm subsetp-union-1
(subsetp x (union$ x y)))
(defthm unit-propagation-correct-1
(implies (formula-truep formula assignment)
(formula-truep
formula
(union$ assignment
(negate-clause-or-assignment clause))))
:hints (("Goal" :restrict ((truth-monotone ((a1 assignment))))))
:rule-classes nil)
(defthm unit-propagation-correct-2
(implies (and (formula-p formula)
(clause-or-assignment-p clause)
(clause-or-assignment-p assignment)
(equal (unit-propagation formula
indices
(negate-clause-or-assignment clause))
t)
(not (equal (evaluate-clause clause assignment)
t)))
(equal (unit-propagation formula
indices
(union$ assignment
(negate-clause-or-assignment clause)))
t))
:rule-classes nil)
(defthm unit-propagation-correct
(implies (and (formula-p formula)
(clause-or-assignment-p clause)
(clause-or-assignment-p assignment)
(formula-truep formula assignment)
(equal (unit-propagation formula
indices
(negate-clause-or-assignment clause))
t))
(equal (evaluate-clause clause assignment)
t))
:hints (("Goal"
:do-not-induct t
:use (unit-propagation-correct-1 unit-propagation-correct-2)
:in-theory (disable formula-p subsetp-union-equal-2))))
|
