qubo_lab/util/randomSAT.py

#!/usr/bin/env python3

import numpy as np
import random
from . import kSAT

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)
    
    #fill in the missing bindings
    for clause in 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])
        
            if tmpClause not in clauses:
                clauseIsUnique = True
                
        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