import random
import copy
import math
import sys
def generate_all_values(args_dict):
args_dict_keys = list(args_dict.keys())
args_dict_keys.sort()
if len(args_dict) == 0:
return [[]]
tmp_values = [0] * len(args_dict_keys)
for x in range(0, 2**len(args_dict)):
tmp_values = copy.deepcopy(tmp_values)
if x == 0:
yield tmp_values
for n in range(0, len(args_dict)):
if tmp_values[n] == 0:
tmp_values[n] = 1
for t in range(0, n):
tmp_values[t] = 0
break
yield tmp_values
def test_3sat_real(clause_number, args_dict):
global good_assignments
good_assignments = []
string_clause = ""
for clause in clause_number:
tmp_string_clause = ""
for counter in range(len(clause[1])):
if clause[0][counter]:
tmp_string_clause += clause[1][counter] + "+"
else:
tmp_string_clause += "!" + clause[1][counter] + "+"
string_clause += "(" + tmp_string_clause[:-1] + ")^"
print(string_clause[:-1])
args_dict_keys = list(args_dict.keys())
args_dict_keys.sort()
good_assignments = []
dividend = math.pow(2, len(args_dict) - 5)
index = 0
args_dict_tmp = copy.deepcopy(args_dict)
for tmp_values in generate_all_values(args_dict_tmp):
for arg in args_dict_keys:
if arg not in args_dict_tmp:
tmp_values.insert(args_dict_keys.index(arg), 0)
final_result = 1
final_result_string = ""
for clause in clause_number:
tmp_final_result = calculate_real_clause_list(clause, args_dict_keys, tmp_values)
if tmp_final_result == 0:
break
final_result_string += str(tmp_final_result) + "^"
final_result &= tmp_final_result
if final_result == 1 and tmp_final_result == 1:
good_assignments.append(tmp_values)
index += 1
if index % dividend == 0:
print(f"index {index}")
print("Number goods: " + str(len(good_assignments)))
return good_assignments
def calculate_real_clause_list(clause, args_keys, args_values):
result = 0
for counter in range(0, len(clause[0])):
index = args_keys.index(clause[1][counter])
arg = args_values[index]
if not clause[0][counter]:
if arg:
arg = 0
else:
arg = 1
result |= arg
return result
def generate_real_clause(*args_list):
args_number = 3 #random.randint(1, len(args_list))
args_clause = [0] * args_number
args_litteral = [0] * args_number
for count in range(args_number):
args_clause[count] = random.randint(0, 1)
argument = args_list[random.randint(0, len(args_list) - 1)]
while argument in args_litteral:
argument = args_list[random.randint(0, len(args_list) - 1)]
args_litteral[count] = argument
tmp_args_litteral = args_litteral.copy()
tmp_args_litteral.sort()
tmp_args_clause = [0] * args_number
for counter in range(0, len(tmp_args_litteral)):
tmp_args_clause[counter] = args_clause[args_litteral.index(tmp_args_litteral[counter])]
return tmp_args_clause, tmp_args_litteral
def gen_3sat_clause(args_dict, clause_n):
clause_number = [[]] * clause_n
for count in range(len(clause_number)):
tmp_clause = generate_real_clause(*args_dict)
while tmp_clause in clause_number:
tmp_clause = generate_real_clause(*args_dict)
clause_number[count] = tmp_clause
string_clause = ""
for clause in clause_number:
tmp_string_clause = ""
for counter in range(len(clause[1])):
if clause[0][counter]:
tmp_string_clause += clause[1][counter] + "+"
else:
tmp_string_clause += "!" + clause[1][counter] + "+"
string_clause += "(" + tmp_string_clause[:-1] + ")^"
print(string_clause[:-1])
print("============================================")
return clause_number
def find_solution(clause_number, args_dict, number_real, quick=False):
print("Clause:", clause_number)
string_clause = ""
for clause in clause_number:
tmp_string_clause = ""
for counter in range(len(clause[1])):
if clause[0][counter]:
tmp_string_clause += clause[1][counter] + "+"
else:
tmp_string_clause += "!" + clause[1][counter] + "+"
string_clause += "(" + tmp_string_clause[:-1] + ")^"
print("Clause", string_clause)
assignment_excluded = []
for clause in clause_number:
tmp_assignment = {}
for counter in range(len(clause[1])):
if clause[0][counter]:
tmp_assignment[clause[1][counter]] = 0
else:
tmp_assignment[clause[1][counter]] = 1
assignment_excluded.append(tmp_assignment)
good_list_tmp = {}
for x in args_dict.keys():
for y in args_dict.keys():
for z in args_dict.keys():
if x != y and x != z and y != z:
key = [x, y, z]
key.sort()
if tuple(key) not in good_list_tmp.keys():
good_list_tmp[tuple(key)] = [[0, 0, 0], [0, 0, 1], [0, 1, 0], [0, 1, 1],
[1, 0, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1]]
full_key = list(args_dict.keys())
full_key.sort()
print("Arguments", full_key)
good_list = []
good_list_debug = []
full_three = list(good_list_tmp.keys())
for g_key in good_list_tmp:
for t_val in good_list_tmp[g_key]:
tmp_val = []
for f_key in full_key:
if f_key in g_key:
tmp_val.append(t_val[g_key.index(f_key)])
else:
tmp_val.append(-1)
good_list.append(tmp_val)
good_list_debug.append([t_val, g_key])
expression_list = []
for assignment in assignment_excluded:
keys = list(assignment.keys())
keys.sort()
values = []
for key in keys:
values.append(assignment[key])
expression_list.append((tuple(keys), values))
assignment_found = []
good_to_remove = []
print("Length of list before exclude", len(good_list))
print("Expresion list", expression_list)
for good_value in good_list:
for keys, values, in expression_list:
for index_key, expression_key in enumerate(keys):
if good_value[full_key.index(expression_key)] != values[index_key]:
break
else:
if keys not in assignment_found:
assignment_found.append(keys)
if good_value not in good_to_remove:
good_to_remove.append(good_value)
for good in good_to_remove:
good_list_debug.pop(good_list.index(good))
good_list.remove(good)
print("Length of list after exclude", len(good_list))
good_list_not = []
good_list_debug_not = []
for step in range(0, len(full_key) - 1):
print(step)
was_changed = False
goods_to_remove = []
good_list_not_add = []
for good_value in good_list:
for expression_keys, expression_value in expression_list:
vals_found = 0
key_not_found = None
for index_key, expression_key in enumerate(expression_keys):
if good_value[full_key.index(expression_key)] == expression_value[index_key]:
vals_found += 1
elif good_value[full_key.index(expression_key)] == -1:
key_not_found = expression_key
if vals_found == (len(expression_keys) - 1) and key_not_found:
if expression_value[expression_keys.index(key_not_found)] == 0:
good_value[full_key.index(key_not_found)] = 1
else:
good_value[full_key.index(key_not_found)] = 0
elif vals_found == len(expression_keys):
goods_to_remove.append(good_value)
else:
continue
was_changed = True
break
else:
good_list_not_add.append(good_value)
for good_to_add in good_list_not_add:
good_list_debug_not.append(good_list_debug[good_list.index(good_to_add)])
good_list_debug.pop(good_list.index(good_to_add))
good_list_not.append(good_to_add)
good_list.remove(good_to_add)
for good_to_remove in goods_to_remove:
good_list_debug.pop(good_list.index(good_to_remove))
good_list.remove(good_to_remove)
if not was_changed:
break
for indx, good in enumerate(good_list_not):
good_list.append(good)
good_list_debug.append(good_list_debug_not[indx])
print("len after", len(good_list))
threes_analyze = {}
for val, key in good_list_debug:
# if len(val) < 8:
# print(key, val)
for three in full_three:
for three_s in three:
if three_s not in key:
break
else:
if three not in threes_analyze:
threes_analyze[three] = []
if val not in threes_analyze[three]:
threes_analyze[three].append(val)
for key in full_three:
if key not in threes_analyze:
print("Key is missing. No solution", key)
return False
three_to_three_double = {}
three_to_three_one = {}
for three_1 in threes_analyze:
three_to_three_double[three_1] = []
three_to_three_one[three_1] = []
for three_2 in threes_analyze:
counter = 0
three_in = []
three_not_in = []
for indx, three_2_s in enumerate(three_2):
if three_2_s in three_1:
counter += 1
three_in.append([three_2_s, indx])
else:
three_not_in.append([three_2_s, indx])
if counter == 2:
three_to_three_double[three_1].append([three_2, three_in, three_not_in])
if counter == 1:
three_to_three_one[three_1].append([three_2, three_in, three_not_in])
for i in range(0, len(full_key)):
print("Cleaning step", i)
was_not_in = False
counter_clean = 0
for three in threes_analyze:
val_to_remove = []
for val in threes_analyze[three]:
double_list = {}
one_list = {}
was_removed = False
for three_c, three_in, three_not_in in three_to_three_one[three]:
double_key = (three_not_in[0][0], three_not_in[1][0])
double_tmp = []
was_in = False
for val_c in threes_analyze[three_c]:
if val_c[three_in[0][1]] == val[three.index(three_in[0][0])]:
double_tmp.append([val_c[three_not_in[0][1]], val_c[three_not_in[1][1]]])
was_in = True
if not was_in:
if val not in val_to_remove:
val_to_remove.append(val)
was_removed = True
if double_key not in double_list:
double_list[double_key] = double_tmp
else:
to_rem = []
for double_val in double_list[double_key]:
if double_val not in double_tmp:
to_rem.append(double_val)
for rem in to_rem:
double_list[double_key].remove(rem)
if not double_list[double_key]:
if val not in val_to_remove:
val_to_remove.append(val)
was_removed = True
if was_removed:
break
if was_removed:
break
for three_c, three_in, three_not_in in three_to_three_double[three]:
one_key = (three_not_in[0][0])
one_tmp = []
was_in = False
for val_c in threes_analyze[three_c]:
if (val_c[three_in[0][1]] == val[three.index(three_in[0][0])]
and val_c[three_in[1][1]] == val[three.index(three_in[1][0])]):
was_in = True
one_tmp.append(val_c[three_not_in[0][1]])
if not was_in:
if val not in val_to_remove:
val_to_remove.append(val)
was_removed = True
if one_key not in one_list:
one_list[one_key] = one_tmp
else:
to_rem = []
for one_val in one_list[one_key]:
if one_val not in one_tmp:
to_rem.append(one_val)
for rem in to_rem:
one_list[one_key].remove(rem)
if not one_list[one_key]:
if val not in val_to_remove:
val_to_remove.append(val)
was_removed = True
if was_removed:
break
tmp_keys = {}
for double_key in double_list:
one_tmp_1 = []
one_tmp_2 = []
for val_l in double_list[double_key]:
if val_l[0] not in one_tmp_1:
one_tmp_1.append(val_l[0])
if val_l[1] not in one_tmp_2:
one_tmp_2.append(val_l[1])
if double_key[0] not in tmp_keys:
tmp_keys[double_key[0]] = one_tmp_1
else:
to_rem = []
for one_t in tmp_keys[double_key[0]]:
if one_t not in one_tmp_1:
to_rem.append(one_t)
for rem in to_rem:
tmp_keys[double_key[0]].remove(rem)
if double_key[1] not in tmp_keys:
tmp_keys[double_key[1]] = one_tmp_2
else:
to_rem = []
for one_t in tmp_keys[double_key[1]]:
if one_t not in one_tmp_2:
to_rem.append(one_t)
for rem in to_rem:
tmp_keys[double_key[1]].remove(rem)
for tmp in tmp_keys:
if not tmp_keys[tmp]:
if val not in val_to_remove:
val_to_remove.append(val)
for val in val_to_remove:
threes_analyze[three].remove(val)
if len(threes_analyze[three]) == 0:
print("Missing key. No solution", three)
return False
counter_clean += 1
was_not_in = True
print("Counter clean", counter_clean)
if not was_not_in:
print("was not in")
break
if quick:
return True
del three_to_three_double
del three_to_three_one
print("Good three list clean")
# for three in threes_analyze:
# print(three, threes_analyze[three])
print("----")
print("------------------- three vals after excluding")
final_good_first = [-1] * len(full_key)
first_three = (full_key[0], full_key[1], full_key[2])
first_three_val = threes_analyze[first_three][0]
final_good_first[0] = first_three_val[0]
final_good_first[1] = first_three_val[1]
final_good_first[2] = first_three_val[2]
final_good = find_final(final_good_first, first_three, threes_analyze,
full_key, assignment_excluded, clause_number)
print("Full key", full_key)
print("Final good:", final_good)
final_result = 1
for clause in clause_number:
tmp_final_result = calculate_real_clause_list(clause, full_key, final_good)
print("Clause", clause, tmp_final_result)
final_result &= tmp_final_result
if final_result == 0:
print("Final value does not solve the 3-SAT expression but should")
exit(1)
return True
def check_if_good(tmp_final_good, full_key, assignment_excluded):
min_values_minus_excluded = []
for ass_exc in assignment_excluded:
not_good = {}
for ass in ass_exc:
if tmp_final_good[full_key.index(ass)] == -1:
if ass_exc[ass] == 0:
not_good[ass] = 1
else:
not_good[ass] = 0
#not_good[ass] = ass_exc[ass]
elif ass_exc[ass] != tmp_final_good[full_key.index(ass)]:
break
else:
#print(ass_exc)
if not_good and not_good not in min_values_minus_excluded:
min_values_minus_excluded.append(not_good)
clauses = []
for min_values_minus in min_values_minus_excluded:
clause = ([], [])
for min in min_values_minus:
clause[1].append(min)
clause[1].sort()
for cl in clause[1]:
clause[0].append(min_values_minus[cl])
clauses.append(clause)
args_dict = {}
for indx, tmp_val in enumerate(tmp_final_good):
if tmp_val == -1:
args_dict[full_key[indx]] = 0
print(min_values_minus_excluded)
return find_solution(clauses, args_dict, [], quick=True)
def check_tmp_final(tmp_final_good, threes_analyze, full_key):
for three_c in threes_analyze:
three_in = []
for three_c_s in three_c:
if tmp_final_good[full_key.index(three_c_s)] != -1:
three_in.append(three_c_s)
if three_in:
is_good = False
for val_c in threes_analyze[three_c]:
for three_c_s in three_in:
if val_c[three_c.index(three_c_s)] != tmp_final_good[full_key.index(three_c_s)]:
break
else:
is_good = True
if not is_good:
print("is good false", three_c, threes_analyze[three_c])
return False
return True
def find_final(tmp_final_good, first_three, threes_analyze, full_key, assignment_excluded, clause_number):
print("First three", first_three)
for key in full_key[3:]:
current_three = (first_three[0], first_three[1], key)
if key == full_key[-3]:
for last_vals in [[0, 0, 0], [0, 0, 1], [0, 1, 0], [0, 1, 1],
[1, 0, 0], [1, 0, 1], [1, 1, 0], [1, 1, 1]]:
tmp_final_last = copy.deepcopy(tmp_final_good)
tmp_final_last[-3] = last_vals[0]
tmp_final_last[-2] = last_vals[1]
tmp_final_last[-1] = last_vals[2]
final_result = 1
for clause in clause_number:
tmp_final_result = calculate_real_clause_list(clause, full_key, tmp_final_last)
# print("Clause", clause, tmp_final_result)
final_result &= tmp_final_result
if final_result == 0:
print("Final candidate value does not solve the 3-SAT expression")
else:
return tmp_final_last
else:
print("No assignment")
exit(1)
candidates = []
for val in threes_analyze[current_three]:
if val[0] == tmp_final_good[0] and val[1] == tmp_final_good[1]:
candidates.append(val[2])
print(candidates)
if len(candidates) == 1:
tmp_final_good[full_key.index(key)] = candidates[0]
else:
for candidate in candidates:
tmp_final = copy.deepcopy(tmp_final_good)
print("Run for ", tmp_final, current_three, current_three, candidate)
tmp_final[full_key.index(key)] = candidate
if check_tmp_final(tmp_final, threes_analyze, full_key):
if check_if_good(tmp_final, full_key, assignment_excluded):
tmp_final_good = tmp_final
print("Is good", tmp_final)
break
print("Is not good", tmp_final)
else:
print("No solution")
exit(1)
return tmp_final_good
def parse_cnf(args_dict, cnf_file):
full_key = list(args_dict.keys())
full_key.sort()
expression = []
with open(cnf_file) as file:
lines = file.read().split("\n")[8:-4]
for line in lines:
args = line.strip().split(" ")[:-1]
subexpression = ([], [])
print(args)
for arg in args:
if "-" in arg:
subexpression[0].append(0)
else:
subexpression[0].append(1)
subexpression[1].append(full_key[int(arg.replace("-", "")) - 1])
expression.append(subexpression)
return expression
def gen_args(number_arguments):
args_dict = {}
counter = 0
for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o']:
for i in [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]:
args_dict["%s%s" % (var, i)] = 0
counter += 1
if counter >= number_arguments:
return args_dict
print("Too much args")
exit(1)
def main():
args_dict = {}
#for var in ["a", "x"]:
#for var in ["a", "b", "c"]:+
#for var in ["a", "x", "y", "u"]:
#for var in ["a", "b", "c", "d", "e"]:
#for var in ["a", "b", "c", "d", "e", "f"]:
#for var in ["a", "b", "c", "d", "e", "f", "g", "h"]:
#for var in ['a', 'b', 'c', 'd', 'e', 'u', 'w', 'x']:
for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j']:
#for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l']:
#for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'u', 'w', 'x', 'y', 'z']:
#for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm']:
#for var in ['a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o']:
#for i in [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]:
#for i in [1, 2, 3, 4, 5, 6, 7, 8]:
#for i in [1, 2, 3, 4, 5, 6]:
for i in [1, 2, 3, 4, 5]:
#for i in [1, 2, 3, 4]:+
#for i in [1, 2, 3]:
#for i in [1, 2]:
#for i in [1]:
args_dict["%s%s" % (var, i)] = 0
print(sys.argv)
if sys.argv[1]:
if sys.argv[2]:
args_dict = gen_args(int(sys.argv[2]))
expression = parse_cnf(args_dict, sys.argv[1])
else:
expression = gen_3sat_clause(args_dict, 255) # 45)
print("Expression", expression)
#expression = [([1, 1, 0], ['b1', 'b4', 'j1']), ([1, 0, 1], ['b1', 'c2', 'e1']), ([1, 0, 1], ['a4', 'd3', 'h4']), ([0, 0, 1], ['a2', 'e2', 'e3']), ([1, 0, 1], ['b1', 'i3', 'j3']), ([1, 1, 1], ['a3', 'e3', 'i3']), ([0, 0, 1], ['d1', 'i4', 'j4']), ([0, 0, 0], ['c1', 'e1', 'g3']), ([1, 0, 0], ['e1', 'e2', 'g3']), ([1, 0, 1], ['b1', 'b3', 'f4']), ([0, 1, 1], ['f2', 'g1', 'i1']), ([0, 0, 1], ['f2', 'f4', 'g3']), ([0, 1, 0], ['d3', 'j1', 'j2']), ([0, 1, 1], ['b2', 'd3', 'i3']), ([1, 1, 0], ['c4', 'd4', 'g2']), ([0, 1, 1], ['b4', 'h3', 'i1']), ([1, 1, 1], ['c3', 'c4', 'j4']), ([1, 1, 1], ['a3', 'f2', 'h2']), ([0, 0, 1], ['b2', 'd3', 'i1']), ([0, 0, 0], ['h1', 'h2', 'h3']), ([0, 1, 1], ['a1', 'd2', 'f2']), ([1, 0, 1], ['b4', 'e2', 'g3']), ([0, 0, 1], ['a3', 'd2', 'g3']), ([1, 0, 1], ['f4', 'h3', 'j2']), ([0, 1, 1], ['b1', 'b4', 'f1']), ([1, 1, 1], ['c3', 'f3', 'g4']), ([0, 1, 1], ['a2', 'b1', 'b4']), ([1, 0, 0], ['a3', 'a4', 'j3']), ([0, 0, 1], ['d2', 'j1', 'j2']), ([1, 1, 1], ['a2', 'a4', 'c3']), ([1, 0, 1], ['b1', 'e3', 'j3']), ([1, 0, 0], ['e2', 'f2', 'g4']), ([1, 1, 1], ['a3', 'h3', 'j3']), ([0, 0, 1], ['c4', 'd3', 'f1']), ([1, 0, 0], ['c4', 'h2', 'i1']), ([1, 1, 0], ['a2', 'b3', 'i4']), ([0, 0, 1], ['a2', 'i3', 'j4']), ([1, 1, 1], ['c3', 'h1', 'j2']), ([0, 1, 1], ['d2', 'g2', 'i1']), ([0, 1, 1], ['c3', 'h1', 'j2']), ([0, 1, 0], ['b2', 'd1', 'j3']), ([1, 0, 1], ['a1', 'b1', 'h1']), ([1, 1, 1], ['b1', 'e1', 'e3']), ([0, 1, 0], ['c4', 'e3', 'j4']), ([0, 0, 0], ['f4', 'h2', 'j2']), ([1, 0, 0], ['e1', 'i2', 'j3']), ([1, 1, 0], ['c2', 'i2', 'j4']), ([1, 1, 0], ['f1', 'g2', 'i1']), ([0, 1, 0], ['b2', 'f3', 'j4']), ([0, 1, 0], ['d3', 'g3', 'h1']), ([1, 1, 1], ['e3', 'f1', 'g3']), ([0, 1, 0], ['f4', 'h1', 'h2']), ([0, 0, 0], ['c4', 'g2', 'i1']), ([0, 1, 0], ['d3', 'e3', 'h4']), ([1, 1, 0], ['b3', 'd1', 'e3']), ([1, 1, 1], ['a3', 'b4', 'f3']), ([1, 1, 0], ['g3', 'i1', 'i4']), ([0, 0, 1], ['a3', 'c4', 'f2']), ([1, 1, 1], ['b2', 'd4', 'j4']), ([0, 1, 1], ['d4', 'g2', 'i2']), ([0, 0, 0], ['f3', 'i1', 'j1']), ([1, 0, 0], ['c2', 'h4', 'j3']), ([1, 1, 0], ['e3', 'f3', 'j3']), ([0, 0, 1], ['a1', 'd3', 'e2']), ([0, 1, 0], ['d2', 'g4', 'h3']), ([1, 1, 0], ['d1', 'e3', 'f1']), ([1, 0, 0], ['d2', 'g1', 'g2']), ([0, 1, 1], ['a1', 'f4', 'h2']), ([0, 1, 1], ['b2', 'e2', 'h2']), ([0, 1, 0], ['c3', 'i3', 'j4']), ([1, 1, 1], ['b3', 'f2', 'i2']), ([1, 1, 1], ['f2', 'g2', 'i1']), ([1, 0, 1], ['b3', 'e1', 'g4']), ([0, 1, 0], ['f4', 'h1', 'h4']), ([1, 0, 1], ['c4', 'd1', 'd4']), ([0, 0, 1], ['c2', 'd4', 'h1']), ([0, 1, 1], ['a2', 'c1', 'c4']), ([1, 0, 0], ['c1', 'g1', 'g3']), ([1, 1, 0], ['a1', 'b4', 'h1']), ([1, 1, 0], ['a3', 'f3', 'i2']), ([1, 0, 1], ['a4', 'f3', 'h2']), ([1, 1, 0], ['a2', 'c3', 'j1']), ([1, 1, 1], ['a1', 'c2', 'c4']), ([0, 1, 0], ['c4', 'd3', 'h4']), ([1, 0, 0], ['d1', 'h1', 'j3']), ([1, 0, 0], ['a1', 'f1', 'h2']), ([0, 0, 1], ['b3', 'e1', 'e4']), ([0, 0, 1], ['d1', 'f3', 'h2']), ([0, 1, 0], ['c1', 'g1', 'g4']), ([1, 1, 1], ['a4', 'h4', 'i1']), ([1, 1, 0], ['c3', 'g3', 'g4']), ([0, 0, 1], ['e2', 'f4', 'g1']), ([1, 1, 1], ['a2', 'b2', 'e3']), ([1, 1, 1], ['d2', 'g1', 'i2']), ([0, 0, 0], ['b4', 'c3', 'f2']), ([1, 1, 1], ['f2', 'g2', 'h2']), ([1, 1, 1], ['b2', 'h2', 'i1']), ([0, 1, 1], ['h4', 'j1', 'j4']), ([0, 1, 0], ['a1', 'a2', 'i2']), ([1, 1, 1], ['b3', 'b4', 'd3']), ([1, 0, 0], ['a4', 'e4', 'f4']), ([1, 0, 0], ['b4', 'e1', 'i2']), ([1, 1, 1], ['h2', 'i1', 'j3']), ([0, 1, 1], ['a2', 'a4', 'c2']), ([0, 0, 0], ['c3', 'e1', 'h3']), ([1, 1, 0], ['a4', 'g4', 'i3']), ([1, 0, 1], ['c2', 'd3', 'h1']), ([1, 0, 0], ['b3', 'g2', 'j1']), ([1, 1, 0], ['g3', 'h1', 'i2']), ([0, 1, 0], ['a2', 'c4', 'j4']), ([1, 1, 1], ['a1', 'c4', 'j4']), ([1, 0, 0], ['b4', 'h4', 'j1']), ([0, 0, 0], ['a1', 'e4', 'g2']), ([0, 0, 1], ['b3', 'g3', 'g4']), ([0, 0, 1], ['b3', 'f1', 'i3']), ([1, 0, 0], ['c2', 'd1', 'g4']), ([1, 0, 1], ['a1', 'c1', 'f4']), ([0, 1, 1], ['c4', 'i1', 'j2']), ([1, 0, 1], ['a2', 'c4', 'e3']), ([0, 1, 0], ['a1', 'b2', 'j3']), ([1, 1, 1], ['d4', 'e4', 'h4']), ([1, 0, 0], ['b1', 'h1', 'i1']), ([1, 0, 0], ['d1', 'd4', 'g2']), ([0, 0, 1], ['a1', 'b1', 'e3']), ([1, 1, 1], ['a1', 'd1', 'd4']), ([1, 1, 1], ['g2', 'g4', 'h4']), ([0, 0, 1], ['b2', 'd3', 'h3']), ([0, 1, 1], ['a4', 'h3', 'i1']), ([1, 1, 0], ['a3', 'a4', 'b4']), ([0, 0, 1], ['a1', 'b3', 'i1']), ([1, 1, 1], ['c4', 'd1', 'i1']), ([1, 0, 1], ['f1', 'g1', 'j1']), ([1, 0, 0], ['c2', 'g3', 'h2']), ([1, 0, 1], ['c3', 'f4', 'i3']), ([1, 0, 1], ['e1', 'g4', 'h3']), ([1, 1, 0], ['a1', 'g1', 'i2']), ([0, 1, 0], ['b2', 'e4', 'g3']), ([1, 0, 1], ['b3', 'b4', 'f2']), ([1, 1, 0], ['f3', 'g1', 'i3']), ([0, 0, 0], ['b1', 'c4', 'd4']), ([1, 1, 0], ['c2', 'd1', 'h4']), ([0, 0, 1], ['f2', 'h1', 'h4']), ([1, 0, 0], ['d1', 'e4', 'g1']), ([0, 0, 1], ['b1', 'c4', 'i3']), ([1, 0, 0], ['d2', 'f4', 'g3']), ([0, 1, 0], ['c3', 'f3', 'i4']), ([1, 1, 0], ['d3', 'g3', 'i3']), ([1, 0, 1], ['e1', 'f1', 'f3']), ([1, 1, 1], ['b2', 'e4', 'f3']), ([1, 1, 0], ['a1', 'a3', 'd4']), ([0, 0, 0], ['a2', 'a3', 'd1']), ([1, 1, 1], ['c3', 'g2', 'i4']), ([1, 0, 0], ['h4', 'i1', 'i4']), ([0, 0, 1], ['g2', 'i1', 'j1']), ([0, 1, 1], ['c2', 'd4', 'j1'])]
#number_real = test_3sat_real(expression, args_dict)
number_real = []
#print("Number real: ", len(number_real), str(number_real[:10]))
find_solution(expression, args_dict, number_real)
if __name__ == "__main__":
main()