These are couple of my remakes of Donald Knuth's SAT0W SAT solver (CWEB file on his website), which is very basic and only serves as a demonstration of watch lists. Read more about it in TAOCP 7.2.2.2 (algorithm B, pp. 30-31).
In short:
#!/usr/bin/env python import sys def read_text_file (fname): with open(fname) as f: content = f.readlines() return [x.strip() for x in content] def read_DIMACS (fname): content=read_text_file(fname) header=content[0].split(" ") assert header[0]=="p" and header[1]=="cnf" variables_total, clauses_total = int(header[2]), int(header[3]) # array idx=number (of line) of clause # val=list of terms # term can be negative signed integer clauses=[] for c in content[1:]: if c.startswith ("c "): continue clause=[] for var_s in c.split(" "): var=int(var_s) if var!=0: clause.append(var) clauses.append(clause) if clauses_total != len(clauses): print "warning: header says ", clauses_total, " but read ", len(clauses) return variables_total, clauses # variable numbers and corresponding literal numbers (the last bit is 1 for a positive variable and 0 for a negative variable): # -1 : 0 # 1 : 1 # -2 : 2 # 2 : 3 # -3 : 4 # 3 : 5 # etc def var2lit(var): if var<0: return (abs(var)-1)*2 else: return (abs(var)-1)*2+1 variables_total, clauses = read_DIMACS(sys.argv[1]) literals_total = variables_total*2 # key = literal # val = watched list of clauses literals={} for l in range(literals_total): literals[l]=[] # set initial watched lists by attaching first variable of each clause to the corresponding literal # first literal/variable of each clause is the default watchee c_no=0 for clause in clauses: first_var=clause[0] l=var2lit(first_var) literals[l].append(c_no) c_no=c_no+1 # array of choices, 0 for False, 1 for True move=[] # if the variable is already assigned? def var_already_assigned_to_false (var): global move return move[abs(var)-1]==0 def var_already_assigned_to_true (var): global move return move[abs(var)-1]==1 # find a place for a clause to reattach it def find_better_place_for_clause(level, c_no): global clauses, move, literals, variables_total if len(clauses[c_no])==1: # unit clause? we can't do anything return False # enumerate all literals/variables in clause except first: for v in range(1, len(clauses[c_no])): var=clauses[c_no][v] # this variable/literal isn't yet assigned # so we can "postpone" it for future if (abs(var)-1) > level: # reattach clause: literals[var2lit(var)].append(c_no) # swap first variable/literal in clause with newly watchee clauses[c_no][v], clauses[c_no][0] = clauses[c_no][0], clauses[c_no][v] return True # this variable/literal is already assigned and it's value coincides with our variable: cond1 = var_already_assigned_to_false(var) and var<0 cond2 = var_already_assigned_to_true(var) and var>0 if cond1 or cond2: # reattach clause: literals[var2lit(var)].append(c_no) # swap first variable/literal in clause with newly watchee clauses[c_no][v], clauses[c_no][0] = clauses[c_no][0], clauses[c_no][v] return True return False # "disembowel" a watch list by reattaching all clauses in WL to other literals/watch lists: def reconnect_all_clauses(level): global clauses, move, literals, variables_total # which literal to "disembowel"? if move[level]==0: lit=level*2+1 else: lit=level*2 # list of clauses in WL to "disembowel": tmp=literals[lit][:] for i in range(len(tmp)): if find_better_place_for_clause(level, tmp[i]): # delete first element. maybe slow? literals[lit]=literals[lit][1:] else: # there is a contradicted clause we can't reattach, so return False return False # all clauses from WL has been reconnected, proceed further return True def try_bits(level): #print "try_bit(", level, ")" global clauses, move, literals, variables_total #print move if level==variables_total: # all variables are assigned, and we are here, hence, all satisfied, so we stop here print "SAT" s="" for i in range(variables_total): if move[i]==1: s=s+str(i+1)+" " else: s=s+"-"+str(i+1)+" " print s exit(0) # if the "positive" literal has a watch list attached, start with True, then switch to False # because there is a chance after backtrack that "negative" literal has no watch list attached, so why do unneeded work # by reattaching? # otherwise, start with False and switch to True if len(literals[level*2+1])>0: first_alternative, second_alternative = 1,0 else: first_alternative, second_alternative = 0,1 move.append(first_alternative) # try to reconnect all clauses # proceed deeper in case of success if reconnect_all_clauses(level): try_bits(level+1) # no success, remove first_alternative from move[], proceed to the second one: move=move[:-1] move.append(second_alternative) if reconnect_all_clauses(level): try_bits(level+1) move=move[:-1] # no luck with both alternatives, so we backtrack by returning from recursive call # if there is no place to return (level=0), the instance cannot be satisfied: if level==0: print "UNSAT" exit(0) try_bits(level=0)
It can solve tiny SAT instances such as queens on a 10*10 chess board, etc.
Now my second solver in C/C++, which works almost like Donald Knuth's SAT0W. My goal was to remake it precisely, so that I can be sure I understood everything well. To be fast, there is no recursion.
Also, as we may notice, clauses are not to be added to a watch list or removed. They are rather moved. Also, order of clauses in watch list is not important at all. Hence, by moving a clause from one WL to another, we can add it to the front of destination WL.
My solution is single-linked lists, but with no pointers, rather indices are stored (and -1 is a terminating value). Like Donald Knuth's SAT0W, my solver can even factorize small 8-bit numbers.
Needless to say, an order of variables influences the process drastically. Hence, my solver can behave differently if it reads DIMACS CNF file or Knuth-style SAT file (where variable names are used instead of numbers). However, finding a best order of variables is a problem comparable to SAL solving itself.
Also, my primitive and naive SAT solver I wrote 2 years ago, but just 120 SLOC.