Skip to content

Commit

Permalink
bla
Browse files Browse the repository at this point in the history
  • Loading branch information
ptgm committed Jun 3, 2024
1 parent 1fd5d18 commit 1fc8508
Show file tree
Hide file tree
Showing 8 changed files with 1,214 additions and 28 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,4 @@
*.bak
.vscode
__pycache__
*.pdf
4 changes: 2 additions & 2 deletions clause.py
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,8 @@ def missing_literals(self) -> list[int]:
return [i for i in range(self.cardinality) if not self.signature[i]]

def __hash__(self) -> int:
""" Hash function for Clause using the bit string. """
return hash(self.signature.to01())
""" Hash function for Clause using the signature bit """
return hash(self.signature.tobytes())

def __eq__(self, other: 'Clause') -> bool:
return isinstance(other, Clause) and \
Expand Down
20 changes: 19 additions & 1 deletion function.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,20 @@ def __init__(self, nvars:int, clauses: Set['Clause']) -> None:
self.nvars = nvars
self.clauses = clauses
self.update_consistency()

@staticmethod
def fromString(nvars: int, strClauses: str) -> 'Function':
if not strClauses:
raise ValueError("Empty function string!")
clauses = set()
for strc in strClauses[2:-2].split("},{"):
if not strc:
raise ValueError("Empty clause!")
tmp = '0'*nvars
for l in strc.split(','):
tmp = tmp[:int(l)-1] + '1' + tmp[int(l):]
clauses.add(Clause(tmp))
return Function(nvars, clauses)

def clone_rm_add(self, scRm: Set['Clause'], scAdd: Set['Clause']) -> 'Function':
f = Function(self.nvars, self.clauses.copy())
Expand Down Expand Up @@ -70,7 +84,11 @@ def __eq__(self, other: 'Function') -> bool:
self.clauses == other.clauses

def __hash__(self) -> int:
return hash(tuple(sorted([c.__hash__() for c in self.clauses])))
# Combine the hashes of the elements using XOR
hash_value = 0
for c in self.clauses:
hash_value ^= hash(c)
return hash_value

def __str__(self) -> str:
return "{" + ",".join(str(c) for c in self.clauses) + "}"
Expand Down
48 changes: 30 additions & 18 deletions hassediagram.py
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,11 @@ class HasseDiagram:
# 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 -> ... functions

def __init__(self, nvars: int) -> None:
self.nvars = nvars
print('----------------', nvars)
self.powerset = PowerSet(nvars)

def get_infimum(self) -> 'Function':
Expand All @@ -36,7 +37,7 @@ def get_size(self) -> int:

def get_f_parents(self, f: 'Function') -> Tuple[Set['Function'], int, int, int]:
""" Returns the set of immediate parents of f. """
fParents = set()
sParents = set()
nR1, nR2, nR3 = 0, 0, 0
# Get maximal independent clauses
sC = self.powerset.get_maximal(self.powerset.get_independent(f.clauses))
Expand All @@ -46,7 +47,7 @@ def get_f_parents(self, f: 'Function') -> Tuple[Set['Function'], int, int, int]:
fp = f.clone_rm_add(set(), {c})
#print('fp:',fp, 'R1')
nR1 += 1
fParents.add(fp)
sParents.add(fp)

# Get maximal dominated clauses
lD = [d for d in self.powerset.get_maximal( \
Expand All @@ -63,42 +64,52 @@ def get_f_parents(self, f: 'Function') -> Tuple[Set['Function'], int, int, int]:
if fp.is_consistent():
#print('fp:',fp,'R2')
nR2 += 1
fParents.add(fp)
sParents.add(fp)
sD.remove(d)
elif len(sContained) == 1:
sTmp = self.powerset.get_dominated_directly(sContained)\
.intersection(sD)
sTmp.remove(d)
for elem in sTmp:
fp = f.clone_rm_add(sContained, {d,elem})
fParents.add(fp)
sParents.add(fp)
nR3 += 1
#print('fp:',fp, 'R3')
sD.remove(d)
return fParents, nR1, nR2, nR3
return sParents, nR1, nR2, nR3

def get_f_children(self, f: 'Function') -> Set['Function']:
def get_f_children(self, f: 'Function') -> Tuple[Set['Function'], int, int, int]:
""" Returns the set of immediate children of f. """
fChildren, dmergeable = set(), {}

sChildren, dmergeable = set(), {}
nR1, nR2, nR3 = 0, 0, 0
# Add all children of the 1st form
for s in f.clauses:
bMergeCand = False
print('s:',s)
bToMerge = False
bIsCandMaxIndpt = True
for l in s.missing_literals():
print(' l:',l+1)
sl = s.clone_add(l)
sAbsorbed = f.getAbsorbed(sl)
print(' absorbed:',sAbsorbed)
if len(sAbsorbed) == 1:
bIsCandMaxIndpt = False
fc = f.clone_rm_add({s}, {sl})
if fc.is_consistent():
#print('fc:',fc, 'R1')
fChildren.add(fc)
print('fc:',fc, 'R2')
nR2+=1
sChildren.add(fc)
elif len(sAbsorbed) == 2:
bMergeCand = True
if bMergeCand:
bToMerge = True
fs = f.clone_rm_add({s},set())
if bIsCandMaxIndpt and fs.is_consistent():
print('fc:',fs,'R1')
nR1+=1
sChildren.add(fs)
elif bToMerge:
sz = s.get_order()
if sz not in dmergeable: dmergeable[sz] = []
dmergeable[sz].append(s)

#print(dmergeable)
for sz in dmergeable:
lmergeable = dmergeable[sz]
while lmergeable:
Expand All @@ -111,7 +122,8 @@ def get_f_children(self, f: 'Function') -> Set['Function']:
if len(sAbsorbed) == 2:
fc = f.clone_rm_add(sAbsorbed, {cl})
#print('fc:',fc, 'R3')
fChildren.add(fc)
nR3+=1
sChildren.add(fc)
lmergeable.pop()

return fChildren
return sChildren, nR1, nR2, nR3
53 changes: 46 additions & 7 deletions main.py
Original file line number Diff line number Diff line change
@@ -1,14 +1,53 @@
from clause import *
from function import *
from hassediagram import *
import random, time, sys

# Testing functions in arXiv paper Fig 5 ##############
n=4
fS1 = Function(n, {Clause('1110'), Clause('1011'), Clause('0111')})
fS2 = Function(n, {Clause('1110'), Clause('0011')})
fS3 = Function(n, {Clause('1101'), Clause('1010'), Clause('0110'), Clause('0011')})
fS4 = Function(n, {Clause('1010'), Clause('0110'), Clause('0011')})
#n=4
#fS1 = Function(n, {Clause('1110'), Clause('1011'), Clause('0111')})
#fS2 = Function(n, {Clause('1110'), Clause('0011')})
#fS3 = Function(n, {Clause('1101'), Clause('1010'), Clause('0110'), Clause('0011')})
#fS4 = Function(n, {Clause('1010'), Clause('0110'), Clause('0011')})

n=3
hd = HasseDiagram(n)
print('Parents[',fS1,']:',hd.get_f_parents(fS1))
print('Childrens[',fS3,']:',hd.get_f_children(fS3))
#print('Parents[',fS1,']:',hd.get_f_parents(fS1))
#print('Childrens[',fS3,']:',hd.get_f_children(fS3))
f1 = Function.fromString(n, '{{2,3},{1}}')
print('f1:', f1)
print('fChildren:', hd.get_f_children(f1))
sys.exit()
#####################################################################
# Testing children vs parents
hd = HasseDiagram(3)

## Random walk from the infimum to the supremum
tracesz = 0
finf = hd.get_infimum()
fsup = hd.get_supremum()
f = finf
t1 = time.time()
while f != fsup:
print('-----------------------------------')
print('f:',f)
sParents, _, _, _ = hd.get_f_parents(f)
lParents = list(sParents)
print('lP:',lParents)
# generate a random int to index the set of parents
i = random.randint(0, len(lParents)-1)
print('lP['+str(i)+']:',lParents[i])
# check parent children -- begin
sChildren, _, _, _ = hd.get_f_children(lParents[i])
print('sC:',sChildren)
if f not in sChildren:
print('.f:', f)
print('.lP[i]:', lParents[i])
print('.lP[i].children:', sChildren)
sys.exit()
# check parent children -- end
f = lParents[i]
tracesz += 1
t2 = time.time()
print('Time:', t2-t1)
print('Sz:', tracesz)
Loading

0 comments on commit 1fc8508

Please sign in to comment.