-
Notifications
You must be signed in to change notification settings - Fork 1
/
CNFSubClause.java
153 lines (119 loc) · 4.38 KB
/
CNFSubClause.java
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
import java.util.HashSet;
import java.util.Iterator;
import java.util.Vector;
/*
* A CNFSubClause in turn consists of a disjunction of literals
*/
public class CNFSubClause implements Comparable<CNFSubClause>
{
//The literals contained in the clause
private HashSet<Literal> literals;
public CNFSubClause()
{
literals = new HashSet<Literal>();
}
public HashSet<Literal> getLiterals()
{
return literals;
}
public Iterator<Literal> getLiteralsList()
{
return literals.iterator();
}
public boolean isEmpty()
{
return literals.isEmpty();
}
public void print()
{
// System.out.println("**************************");
Iterator<Literal> iter = this.getLiteralsList();
System.out.print("(");
while(iter.hasNext())
{
Literal l = iter.next();
l.print();
if(iter.hasNext())
System.out.print(" ");
if(iter.hasNext())
System.out.print("\\/ ");
}
System.out.print(")\n");
}
/* Applies resolution on two CNFSubClauses
* The resulting clause will contain all the literals of both CNFSubclauses
* except the pair of literals that are a negation of each other.
*/
public static Vector<CNFSubClause> resolution(CNFSubClause CNF_SC_1, CNFSubClause CNF_SC_2)
{
Vector<CNFSubClause> newClauses = new Vector<CNFSubClause>();
Iterator<Literal> iter = CNF_SC_1.getLiteralsList();
//The iterator goes through all Literals of the first clause
while(iter.hasNext())
{
Literal l = iter.next();
Literal m = new Literal(l.getName(), !l.getNeg());
//If the second clause contains the negation of a Literal in the first clause
if(CNF_SC_2.getLiterals().contains(m))
{
//We construct a new clause that contains all the literals of both CNFSubclauses...
CNFSubClause newClause = new CNFSubClause();
//...except the pair the literals that were a negation of one another
HashSet<Literal> CNF_SC_1_Lits = new HashSet<Literal>(CNF_SC_1.getLiterals());
HashSet<Literal> CNF_SC_2_Lits = new HashSet<Literal>(CNF_SC_2.getLiterals());
CNF_SC_1_Lits.remove(l);
CNF_SC_2_Lits.remove(m);
//Normally we have to remove duplicates of the same literal; the new clause must not contain the same literal more than once
//But since we use HashSet only one copy of a literal will be contained anyway
newClause.getLiterals().addAll(CNF_SC_1_Lits);
newClause.getLiterals().addAll(CNF_SC_2_Lits);
newClauses.add(newClause);
}
}//The loop runs for all literals, producing a different new clause for each different pair of literals that negate each other
return newClauses;
}
//Override
public boolean equals(Object obj)
{
CNFSubClause l = (CNFSubClause)obj;
Iterator<Literal> iter = l.getLiteralsList();
while(iter.hasNext())
{
Literal lit = iter.next();
if(!this.getLiterals().contains(lit))
return false;
}
if(l.getLiterals().size() != this.getLiterals().size())
return false;
return true;
}
//@Override
public int hashCode()
{
Iterator<Literal> iter = this.getLiteralsList();
int code = 0;
while(iter.hasNext())
{
Literal lit = iter.next();
code = code + lit.hashCode();
}
return code;
}
//@Override
public int compareTo(CNFSubClause x)
{
int cmp = 0;
Iterator<Literal> iter = x.getLiteralsList();
while(iter.hasNext())
{
Literal lit = iter.next();
Iterator<Literal> iter2 = this.getLiterals().iterator();
while(iter2.hasNext())
{
Literal lit2 = iter2.next();
cmp = cmp + lit.compareTo(lit2);
}
}
return cmp;
}
}