You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
59 lines
1.5 KiB
59 lines
1.5 KiB
#!/usr/bin/env python3
|
|
|
|
from util import randomSAT as rdSAT
|
|
import matplotlib.pyplot as plt
|
|
import seaborn as sns
|
|
|
|
import numpy as np
|
|
|
|
def test1():
|
|
kSATInstance = rdSAT.generateRandomKSAT(5, 4, 3)
|
|
|
|
print(kSATInstance.toString())
|
|
|
|
print("conflicts:")
|
|
|
|
for conflict in kSATInstance.getConflicts():
|
|
conflictVerified = False
|
|
|
|
clause1 = kSATInstance.getClause(conflict[0][0])
|
|
clause2 = kSATInstance.getClause(conflict[1][0])
|
|
|
|
for binding in clause2:
|
|
if binding == conflict[0][1] * -1:
|
|
conflictVerified = True
|
|
|
|
print(conflict[0], conflict[1], conflictVerified)
|
|
|
|
def test2():
|
|
data = {}
|
|
|
|
data["clause"] = []
|
|
data["num"] = []
|
|
data["labels"] = []
|
|
|
|
for i in range(10000):
|
|
sat = rdSAT.generateRandomKSAT(7, 6, 3)
|
|
|
|
for ci in range(sat.getNumberOfClauses()):
|
|
clause = sat.getClause(ci)
|
|
clause = list(np.sort(clause))
|
|
|
|
if clause in data["clause"]:
|
|
clauseIndex = data["clause"].index(clause)
|
|
data["num"][clauseIndex] += 1
|
|
else:
|
|
data["clause"].append(clause)
|
|
data["labels"].append("[{}, {}, {}]".format(clause[0], clause[1], clause[2]))
|
|
data["num"].append(1)
|
|
|
|
|
|
print("done ({}) unique clauses".format(len(data["clause"])))
|
|
|
|
sns.set()
|
|
|
|
sns.barplot(x=data["labels"], y=data["num"])
|
|
|
|
plt.show()
|
|
|
|
test2()
|