This topic was archived here:

https://web.archive.org/web/20230000000000fw_/https://www.zenhax.com/viewtopic.php?t=11606

Alpha1001, posted Wed Jun 19, 2019 1:44 pm (48908)

---

Hi, I've made this prototype using the Python to create a SatSolver, but I cannot to implement the functions. Someone can give a tip to begin the project?
Sorry for my bad english

Here the prototype:
def readInputs ():

inputs = []

return inputs


def readClauses (inputs):

clauses = []

return clauses


def readVariables(clauses):

variables = []

return variables


def readFormula ():

inputs = readInputs()

clauses = readClauses(inputs)

variables = readVariables(clauses)

result = { 'clauses':clauses,
'variables' :variables}

return result


def nextAssignment (currentAssignment)
:

nextAssignment = []

return nextAssignment


def doSolve(clauses, assignment):

isSat = False

while (( not isSat) and '''must check
whether this is the last assignment or
not''' ):

'''does this assignment satisfy the
formula? If so, make isSat true.


if not, get the next assignment and try
again.'''

assignment = nextAssignment
(assignment)

result = { 'isSat' : isSat,
'satisfyingAssignment' : None }

if (isSat):

result[ 'satisfyingAssignment'] =
assignment


return result


def solve ():

formula = readFormula()

result = doSolve(formula[ 'clauses'],
formula[ 'variables' ])

return result