-
Notifications
You must be signed in to change notification settings - Fork 0
/
hassediagram.py
125 lines (108 loc) · 5.2 KB
/
hassediagram.py
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
from clause import *
from function import *
from powerset import *
from typing import Tuple
class HasseDiagram:
# Dedeking number: number of monotone Boolean functions of n variables:
# https://oeis.org/A000372
# Number of monotone non-degenerate Boolean functions of n variables:
# n=2 -> 2 functions
# n=3 -> 9 functions
# n=4 -> 114 functions
# n=5 -> 6 894 functions
# n=6 -> 7 785 062 functions
# n=7 -> 2 414 627 396 434 functions
# n=8 -> 56 130 437 209 370 320 359 966 functions
# n=9 -> 286 386 577 668 298 410 623 295 216 696 338 374 471 993 functions
def __init__(self, nvars: int) -> None:
self.nvars = nvars
self.powerset = PowerSet(nvars)
def get_infimum(self) -> 'Function':
""" Returns the infimum of the set of functions. """
return Function(self.nvars, { Clause('1'*self.nvars) })
def get_supremum(self) -> 'Function':
""" Returns the supremum of the set of functions. """
return Function(self.nvars,
{ Clause('0'*i + '1' + '0'*(self.nvars - 1 - i))
for i in range(self.nvars) } )
def get_size(self) -> int:
""" Returns the number of variables of the Hasse diagram. """
return self.nvars
def get_f_parents(self, f: 'Function') -> Tuple[Set['Function'], Set['Function'], Set['Function']]:
""" Returns the set of immediate parents of f. """
s1Parents, s2Parents, s3Parents = set(), set(), set()
# Get maximal independent clauses
sC = self.powerset.get_maximal(self.powerset.get_independent(f.clauses))
# Add all parents from the 1st rule
s1Parents = { f.clone_rm_add(set(), { c }) for c in sC }
# Get maximal dominated clauses
lD = [d for d in self.powerset.get_maximal( \
self.powerset.get_dominated_directly(f.clauses))\
if not any([(d<=s) for s in sC])]
# Add all parents from the 2nd rule
sDnotUsed = {}
for d in lD:
sContained = d.get_containing(f.clauses)
fp = f.clone_rm_add(sContained, {d})
if fp.is_consistent():
s2Parents.add(fp)
#print(' fp:',fp,'R2')
else:
for s in sContained:
if s not in sDnotUsed: sDnotUsed[s] = set()
sDnotUsed[s].add(d)
# Add all parents from the 3rd rule
for s in sDnotUsed:
lSigmas = list(sDnotUsed[s])
if len(lSigmas) < 2: # needs at least 2 clauses to be combined
continue
for i in range(len(lSigmas)-1):
for j in range(i + 1, len(lSigmas)):
# by def only s contains both sigma_i and sigma_j
fp = f.clone_rm_add({s}, {lSigmas[i],lSigmas[j]})
# by def no need to test if isCover(fp)
s3Parents.add(fp)
#print(' fp:',fp, 'R3')
return s1Parents, s2Parents, s3Parents
def get_f_children(self, f: 'Function') -> Tuple[Set['Function'], Set['Function'], Set['Function']]:
""" Returns the set of immediate children of f. """
s1Children, s2Children, s3Children = set(), set(), set()
dmergeable = {}
# Add all children of the 1st form
for s in f.clauses:
bToMerge, bExtendable = False, False
# Child function to be extended with: s \cup {l_i}
fs = f.clone_rm_add({s},set())
for l in s.get_off_literals():
sl = s.clone_add(l)
sAbsorbed = sl.get_contained(f.clauses)
if len(sAbsorbed) == 1:
bExtendable = True
fs = fs.clone_rm_add(set(), {sl})
elif len(sAbsorbed) == 2:
bToMerge = True
if bExtendable:
s2Children.add(fs)
#print('fc:',fs, 'R2')
elif fs.is_consistent():
s1Children.add(fs)
#print('fc:',fs, 'R1')
elif bToMerge:
# Clauses are only (potentially) mergeable with others of their own size
sz = s.get_order()
if sz not in dmergeable: dmergeable[sz] = []
dmergeable[sz].append(s)
for sz in dmergeable:
lmergeable = dmergeable[sz]
while lmergeable:
c = lmergeable[-1]
fMergeable = Function(f.get_size(), set(lmergeable))
for l in c.get_off_literals():
cl = c.clone_add(l)
sAbsorbed = cl.get_contained(fMergeable.clauses)
if len(sAbsorbed) == 2:
fc = f.clone_rm_add(sAbsorbed, {cl})
s3Children.add(fc)
#print('fc:',fc, 'R3')
lmergeable.pop()
return s1Children, s2Children, s3Children