I am trying to implement a recursive function to solve a 3-SAT problem as described in the this great Udacity course https://www.udacity.com/course/cs313 I am new of Python programming and I have noticed a behavior I find strange.
The fact is that when the recursive3SatSolver ends returning None and the algorithm backtracks to a new branch the solution variable (passed as parameter at each iteration) is not set to the previous state but remains with the latest value (the one modified within the ended function)
it behaves as if the parameter was passed by reference and not by value
def solve_3SAT(num_variables, clauses):
solution = [-1]*(num_variables+1)
satisfiedClauses = [0]*len(clauses)
for i in range(0, num_variables+1):
positive = False
negative = False
for idClause,clause in enumerate(clauses):
positive = positive or (i in clause)
negative = negative or (-i in clause)
candidate = positive ^ negative
for idClause,clause in enumerate(clauses):
if i in clause:
if candidate:
satisfiedClauses[idClause]=1
if candidate:
if positive:
solution[i]=1
else:
solution[i]=0
solution[0]=0
print 'preprocessing: ',solution
solution = recursive3SatSolver(num_variables,solution,clauses)
if solution != None:
for idS,s in enumerate(solution):
if solution[idS]<0:
solution[idS]=0
return solution
def recursive3SatSolver(num_variables, solution, clauses):
if is_satisfiable(clauses,solution)==False:
return None
satisfiedClauses = satisfied_clauses(clauses,solution)
for idC,sat in enumerate(satisfiedClauses):
if sat == 0:
chosenClause=idC
clause = clauses[chosenClause]
for idVar,var in enumerate(clause):
absVar = abs(var)
if solution[absVar]<0:
value=-1
if var>0:
value=1
else:
value=0
solution[absVar]=value
if is_satisfied(num_variables,clauses,solution):
return solution
else:
finalSolution = recursive3SatSolver(num_variables,solution,clauses)
if finalSolution!=None:
#print 'returning ...'
return finalSolution
else:
print 'changing branch: ',solution,'=>'
solution[absVar]=1-solution[absVar]
continue
print 'finished possibilities for this clause'
return None
if is_satisfied(num_variables,clauses,solution):
return solution
else:
print 'no more clauses'
return None
def satisfied_clauses(clauses,assignment):
satisfiedClauses= [0]*len(clauses)
for idClause,clause in enumerate(clauses):
if is_clause_satisfied(clause,assignment):
satisfiedClauses[idClause]=1
return satisfiedClauses
def is_satisfiable(clauses, assignment):
for clause in clauses:
if is_clause_satisfiable(clause,assignment):
continue
else:
return False
return True
def is_clause_satisfiable(clause,assignment):
sat = is_clause_satisfied(clause,assignment)
if sat :
return True
else:
for idVar, var in enumerate(clause):
absVar = abs(var)
if assignment[absVar]==-1:
return True
return False
def is_clause_satisfied(clause,assignment):
for idVar,var in enumerate(clause):
absVar = abs(var)
if assignment[absVar]<0:
continue
if var>0:
if assignment[absVar]==1:
return True
else:
if assignment[absVar]==0:
return True
return False
def is_satisfied(num_variables, clauses, assignment):
if assignment==None:
return False
check=True
for clause in clauses:
clauseVal = False;
for var in clause:
val=False;
if var<0:
val = not assignment[abs(var)]
else:
val = assignment[var]
clauseVal = clauseVal or val
check = check and clauseVal
return check
def test():
clauses = [[-2, -3, -1], [3, -2, 1], [-3, 2, 1],
[2, -3, -1], [3, -2, 1], [3, -2, 1]]
solutions = [[0, 0, 0, 0],
[0, 0, 1, 1],
[0, 1, 0, 0],
[0, 1, 1, 0],
[1, 0, 0, 0],
[1, 0, 1, 1],
[1, 1, 0, 0],
[1, 1, 1, 0]]
assert solve_3SAT(3,clauses) in solutions
clauses = [[2, 1, 3], [-2, -1, 3], [-2, 3, -1], [-2, -1, 3],
[2, 3, 1], [-1, 3, -2], [-3, 2, 1], [1, -3, -2],
[-2, -1, 3], [1, -2, -3], [-2, -1, 3], [-1, -2, -3],
[3, -2, 1], [2, 1, 3], [-3, -1, 2], [-3, -2, 1],
[-1, 3, -2], [1, 2, -3], [-3, -1, 2], [2, -1, 3]]
assert solve_3SAT(3,clauses) == None
print 'Tests passed'
clauses = [[2, 1, 3], [-2, -1, 3], [-2, 3, -1], [-2, -1, 3],
[2, 3, 1], [-1, 3, -2], [-3, 2, 1], [1, -3, -2],
[-2, -1, 3], [1, -2, -3], [-2, -1, 3], [-1, -2, -3],
[3, -2, 1], [2, 1, 3], [-3, -1, 2], [-3, -2, 1],
[-1, 3, -2], [1, 2, -3], [-3, -1, 2], [2, -1, 3]]
assert solve_3SAT(3,clauses) == None
print 'Tests passed'
UPDATE I have been wondering why I have needed some time to get this. And I have understood the reason is that I was used to program back tracking on boolean clauses/predicates in Prolog where the variables are automatically set to the previous step when a branch fail.
