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.
101 lines
3.1 KiB
101 lines
3.1 KiB
#!/usr/bin/env python3
|
|
|
|
import numpy as np
|
|
import random
|
|
from . import kSAT
|
|
import math
|
|
|
|
def generateRandomKSAT(numberOfClauses,
|
|
numberOfVariables,
|
|
numberOfVariablesPerClause):
|
|
|
|
instance = kSAT.kSAT()
|
|
|
|
clauses = [[] for i in range(numberOfClauses)]
|
|
|
|
#make sure every variable is bound to at least one clause
|
|
for varIndex in range(numberOfVariables):
|
|
|
|
clauseIndex = random.choice(range(numberOfClauses))
|
|
|
|
while (len(clauses[clauseIndex]) >= numberOfVariablesPerClause or
|
|
varIndex + 1 in clauses[clauseIndex]):
|
|
clauseIndex = random.choice(range(numberOfClauses))
|
|
|
|
clauses[clauseIndex].append(varIndex + 1)
|
|
|
|
for i in range(len(clauses)):
|
|
clauses[i].sort()
|
|
|
|
#fill in the missing bindings
|
|
for clauseIndex, clause in enumerate(clauses):
|
|
tmpClause = []
|
|
|
|
clauseIsUnique = False
|
|
while not clauseIsUnique:
|
|
|
|
tmpClause = clause.copy()
|
|
|
|
numRemainingBindings = numberOfVariablesPerClause - len(tmpClause)
|
|
variablesNotYetInClause = __getVariablesNotYetInClause(tmpClause,
|
|
numberOfVariables)
|
|
|
|
remainingBindings = random.sample(variablesNotYetInClause,
|
|
numRemainingBindings)
|
|
|
|
tmpClause += remainingBindings
|
|
|
|
for i in range(len(tmpClause)):
|
|
tmpClause[i] *= random.choice([-1, 1])
|
|
|
|
tmpClause.sort()
|
|
|
|
if tmpClause not in clauses:
|
|
clauseIsUnique = True
|
|
|
|
clauses[clauseIndex] = tmpClause
|
|
|
|
instance.addClause(tmpClause)
|
|
|
|
return instance
|
|
|
|
|
|
def __getVariablesNotYetInClause(clause, numberOfTotalVars):
|
|
missingVariables = []
|
|
|
|
prevVar = 1;
|
|
for currVar in clause:
|
|
missingVariables += list(range(prevVar, currVar))
|
|
|
|
prevVar = currVar + 1
|
|
|
|
missingVariables += list(range(prevVar, numberOfTotalVars + 1))
|
|
|
|
return missingVariables
|
|
|
|
def number_of_possible_clauses(number_of_variables, variables_per_clause):
|
|
return int(__binom(number_of_variables, variables_per_clause)
|
|
* __number_of_sign_placements(variables_per_clause))
|
|
|
|
def number_of_possible_instances(number_of_clauses,
|
|
number_of_variables,
|
|
variables_per_clause):
|
|
return int(__binom(number_of_possible_clauses(number_of_variables,
|
|
variables_per_clause),
|
|
number_of_clauses))
|
|
|
|
def __binom(n, k):
|
|
if n == k:
|
|
return 1
|
|
elif k == 1:
|
|
return n
|
|
else:
|
|
return math.factorial(n) / (math.factorial(k) * math.factorial(n - k))
|
|
|
|
def __number_of_sign_placements(variables_per_clause):
|
|
result = 0;
|
|
|
|
for i in range(variables_per_clause + 1):
|
|
result += __binom(variables_per_clause, i)
|
|
|
|
return result
|