import random
import copy
import math
import sys
import argparse
from multiprocessing import Pool, Lock
lock = Lock()
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(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 calculate_real_clause_list(clause_number, full_key, candidate):
final_result = 1
for clause in clause_number:
tmp_final_result = calculate_real_clause(clause, full_key, candidate)
# print("Clause", clause, tmp_final_result)
final_result &= tmp_final_result
if final_result == 0:
return False
return True
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 exclude_first(args):
good_list = args[0]
good_list_debug = args[1]
full_key = args[2]
expression_list = args[3]
good_list_not = []
good_list_debug_not = []
for step in range(0, len(full_key) - 1):
if step % 10 == 0:
print(step)
was_changed = False
goods_to_remove = []
good_list_not_add = []
for good_indx, good_value in enumerate(good_list):
#print(expression_list)
for expression_indx, expression_value in expression_list:
vals_found = 0
key_not_found = -1
key_not_found_full = -1
for index_key, expression_in in enumerate(expression_indx):
if good_value[expression_in] == expression_value[index_key]:
vals_found += 1
elif good_value[expression_in] == -1:
key_not_found = index_key
key_not_found_full = expression_in
if vals_found == (len(expression_indx) - 1) and key_not_found != -1:
if expression_value[key_not_found] == 0:
good_value[key_not_found_full] = 1
else:
good_value[key_not_found_full] = 0
elif vals_found == len(expression_indx):
goods_to_remove.append(good_indx)
else:
continue
was_changed = True
break
else:
good_list_not_add.append(good_indx)
good_indexes = {}
for good_to_indx in goods_to_remove:
good_indexes[good_to_indx] = 0
for good_to_indx in good_list_not_add:
good_indexes[good_to_indx] = 1
good_indexes_list = list(good_indexes.keys())
good_indexes_list.sort()
good_indexes_list = list(reversed(good_indexes_list))
for good_indx in good_indexes_list:
if good_indexes[good_indx] == 1:
good_list_debug_not.append(good_list_debug[good_indx])
good_list_not.append(good_list[good_indx])
good_list.pop(good_indx)
good_list_debug.pop(good_indx)
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])
return good_list, good_list_debug
def clean_threes(args):
full_three_part = args[0]
threes_analyze = args[1]
start = args[2]
full_key = args[3]
full_indexes_to_index = args[4]
full_three_to_indexes = args[5]
was_not_in = False
counter_clean = 0
global lock
for index_t, three in enumerate(full_three_part):
vals_to_remove = []
for val in threes_analyze[start+index_t]:
val_to_rem = clean_three([val, threes_analyze, full_key, full_indexes_to_index,
full_three_to_indexes[start+index_t]])
#print(three, val_to_rem)
if val_to_rem:
vals_to_remove.append(val_to_rem)
if not vals_to_remove:
continue
lock.acquire()
try:
#print(three, vals_to_remove, threes_analyze[start+index_t])
for val in vals_to_remove:
threes_analyze[start+index_t].remove(val)
if len(threes_analyze[start+index_t]) == 0:
print("Missing key. No solution", three)
return -1
counter_clean += 1
was_not_in = True
finally:
lock.release()
print("Counter clean", counter_clean)
if not was_not_in:
#print("was not in")
return False
return threes_analyze[start: start+len(full_three_part)], start
def clean_three(args):
val = args[0]
threes_analyze = args[1]
full_key = args[2]
full_indexes_to_index = args[3]
three = args[4]
double_list = []
one_list = []
for _ in range(0, len(full_key)):
one_list.append([0, 0, 0])
for indx_1, _ in enumerate(full_key[:-1]):
double_list.append([])
for indx_2, _ in enumerate(full_key[indx_1+1:]):
double_list[indx_1].append([0, 0, 0, 0, 0])
for indx_1, _ in enumerate(full_key[:-1]):
if indx_1 == three[0] or indx_1 == three[1] or indx_1 == three[2]:
continue
for indx_2 in range(indx_1+1, len(full_key)):
if indx_2 == three[0] or indx_2 == three[1] or indx_2 == three[2] or indx_1 == indx_2:
continue
three_in = []
if indx_1 < three[0] and indx_2 < three[0]:
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[0])], 0, 2, 1, 0, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[1])], 1, 2, 1, 0, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 1, 0, indx_1, indx_2])
elif indx_1 < three[0] and indx_2 < three[1]:
three_in.append([full_indexes_to_index[(indx_1, three[0], indx_2)], 0, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[1])], 1, 2, 0, 1, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 0, 1, indx_1, indx_2])
elif indx_1 < three[0] and indx_2 < three[2]:
three_in.append([full_indexes_to_index[(indx_1, three[0], indx_2)], 0, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[1], indx_2)], 1, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 0, 1, indx_1, indx_2])
elif indx_1 < three[0] and indx_2 > three[2]:
three_in.append([full_indexes_to_index[(indx_1, three[0], indx_2)], 0, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[1], indx_2)], 1, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[2], indx_2)], 2, 1, 0, 2, indx_1, indx_2])
elif indx_1 < three[1] and indx_2 < three[1]:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[1])], 1, 2, 0, 1, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 0, 1, indx_1, indx_2])
elif indx_1 < three[1] and indx_2 < three[2]:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[1], indx_2)], 1, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 0, 1, indx_1, indx_2])
elif indx_1 < three[1] and indx_2 > three[2]:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[1], indx_2)], 1, 1, 0, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[2], indx_2)], 2, 1, 0, 2, indx_1, indx_2])
elif indx_1 < three[2] and indx_2 < three[2]:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(three[1], indx_1, indx_2)], 1, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, indx_2, three[2])], 2, 2, 0, 1, indx_1, indx_2])
elif indx_1 < three[2] and indx_2 > three[2]:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(three[1], indx_1, indx_2)], 1, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(indx_1, three[2], indx_2)], 2, 1, 0, 2, indx_1, indx_2])
else:
three_in.append([full_indexes_to_index[(three[0], indx_1, indx_2)], 0, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(three[1], indx_1, indx_2)], 1, 0, 1, 2, indx_1, indx_2])
three_in.append([full_indexes_to_index[(three[2], indx_1, indx_2)], 2, 0, 1, 2, indx_1, indx_2])
for three_i, three_in_f_1, three_in_1, three_not_in_1, three_not_in_2, three_not_in_f_1, three_not_in_f_2 in three_in:
double_key = (three_not_in_f_1, three_not_in_f_2)
double_tmp = [[-1, -1], [-1, -1]]
was_in = False
for val_c in threes_analyze[three_i]:
if val_c[three_in_1] == val[three_in_f_1]:
double_tmp[val_c[three_not_in_1]][val_c[three_not_in_2]] = 1
was_in = True
if not was_in:
return val
double_key = (double_key[0], double_key[1] - double_key[0] - 1)
if double_list[double_key[0]][double_key[1]][0] == 0:
double_list[double_key[0]][double_key[1]][0] = -1
double_list[double_key[0]][double_key[1]][1] = double_tmp[0][0]
double_list[double_key[0]][double_key[1]][2] = double_tmp[0][1]
double_list[double_key[0]][double_key[1]][3] = double_tmp[1][0]
double_list[double_key[0]][double_key[1]][4] = double_tmp[1][1]
else:
if double_tmp[0][0] == -1:
double_list[double_key[0]][double_key[1]][1] = -1
if double_tmp[0][1] == -1:
double_list[double_key[0]][double_key[1]][2] = -1
if double_tmp[1][0] == -1:
double_list[double_key[0]][double_key[1]][3] = -1
if double_tmp[1][1] == -1:
double_list[double_key[0]][double_key[1]][4] = -1
for d_t in double_list[double_key[0]][double_key[1]]:
if d_t != -1:
break
else:
return val
for indx_one, _ in enumerate(full_key):
if indx_one == three[0] or indx_one == three[1] or indx_one == three[2]:
continue
three_in = []
if indx_one < three[0]:
three_in.append([full_indexes_to_index[(indx_one, three[0], three[1])], 0, 1, 1, 2, 0, indx_one])
three_in.append([full_indexes_to_index[(indx_one, three[0], three[2])], 0, 2, 1, 2, 0, indx_one])
three_in.append([full_indexes_to_index[(indx_one, three[1], three[2])], 1, 2, 1, 2, 0, indx_one])
elif three[0] < indx_one < three[1]:
three_in.append([full_indexes_to_index[(three[0], indx_one, three[1])], 0, 1, 0, 2, 1, indx_one])
three_in.append([full_indexes_to_index[(three[0], indx_one, three[2])], 0, 2, 0, 2, 1, indx_one])
three_in.append([full_indexes_to_index[(indx_one, three[1], three[2])], 1, 2, 1, 2, 0, indx_one])
elif three[1] < indx_one < three[2]:
three_in.append([full_indexes_to_index[(three[0], three[1], indx_one)], 0, 1, 0, 1, 2, indx_one])
three_in.append([full_indexes_to_index[(three[0], indx_one, three[2])], 0, 2, 0, 2, 1, indx_one])
three_in.append([full_indexes_to_index[(three[1], indx_one, three[2])], 1, 2, 0, 2, 1, indx_one])
else:
three_in.append([full_indexes_to_index[(three[0], three[1], indx_one)], 0, 1, 0, 1, 2, indx_one])
three_in.append([full_indexes_to_index[(three[0], three[2], indx_one)], 0, 2, 0, 1, 2, indx_one])
three_in.append([full_indexes_to_index[(three[1], three[2], indx_one)], 1, 2, 0, 1, 2, indx_one])
for three_i, three_in_v_1, three_in_v_2, three_in_1, three_in_2, three_not_in, three_not_in_f_1 in three_in:
one_key = three_not_in_f_1
one_tmp = [-1, -1]
was_in = False
for val_c in threes_analyze[three_i]:
if (val_c[three_in_1] == val[three_in_v_1]
and val_c[three_in_2] == val[three_in_v_2]):
was_in = True
one_tmp[val_c[three_not_in]] = 1
if not was_in:
return val
if one_list[one_key][0] == 0:
one_list[one_key][0] = -1
one_list[one_key][1] = one_tmp[0]
one_list[one_key][2] = one_tmp[1]
else:
if one_tmp[0] == -1:
one_list[one_key][1] = -1
if one_tmp[1] == -1:
one_list[one_key][2] = -1
for d_t in one_list[one_key]:
if d_t != -1:
break
else:
return val
tmp_keys = []
for _ in range(0, len(one_list)):
tmp_keys.append([0, 0, 0])
for double_key_1, _ in enumerate(double_list):
for double_key_2, _ in enumerate(double_list[double_key_1]):
double_key_2_t = double_key_2 + double_key_1 + 1
one_tmp_1 = [-1, -1]
one_tmp_2 = [-1, -1]
if double_list[double_key_1][double_key_2][0] == 0:
continue
if double_list[double_key_1][double_key_2][1] != -1:
one_tmp_1[0] = 1
one_tmp_2[0] = 1
if double_list[double_key_1][double_key_2][2] != -1:
one_tmp_1[0] = 1
one_tmp_2[1] = 1
if double_list[double_key_1][double_key_2][3] != -1:
one_tmp_1[1] = 1
one_tmp_2[0 ]= 1
if double_list[double_key_1][double_key_2][4] != -1:
one_tmp_1[1] = 1
one_tmp_2[1] = 1
if tmp_keys[double_key_1][0] == 0:
tmp_keys[double_key_1][0] = 1
tmp_keys[double_key_1][1] = one_tmp_1[0]
tmp_keys[double_key_1][2] = one_tmp_1[1]
else:
tmp_keys[double_key_1][1] = one_tmp_1[0]
tmp_keys[double_key_1][2] = one_tmp_1[1]
if tmp_keys[double_key_1][1] == -1 and tmp_keys[double_key_1][2] == -1:
return val
if tmp_keys[double_key_2_t][0] == 0:
tmp_keys[double_key_2_t][0] = 1
tmp_keys[double_key_2_t][1] = one_tmp_2[0]
tmp_keys[double_key_2_t][2] = one_tmp_2[1]
else:
tmp_keys[double_key_2_t][1] = one_tmp_2[0]
tmp_keys[double_key_2_t][2] = one_tmp_2[1]
if tmp_keys[double_key_2_t][1] == -1 and tmp_keys[double_key_2_t][2] == -1:
return val
return False
def display_clause(clause_number):
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[:-1])
def get_expression_list(clause_number, full_key):
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)
expression_list = []
#print(full_key)
for assignment in assignment_excluded:
ass_keys = list(assignment.keys())
ass_keys.sort()
#print(ass_keys)
keys = []
for ass_k in ass_keys:
#print(ass_k, full_key.index(ass_k))
keys.append(full_key.index(ass_k))
values = []
for ass_k in ass_keys:
values.append(assignment[ass_k])
#print(keys, values)
expression_list.append((tuple(keys), values))
return expression_list, assignment_excluded
def get_good_and_debug(full_key):
good_list_tmp = {}
for index_x, x in enumerate(full_key[0:-2]):
for index_y, y in enumerate(full_key[index_x+1:-1]):
for z in full_key[index_x+index_y+1:]:
if x != y and x != z and y != z:
key = [x, y, z]
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_three = list(good_list_tmp.keys())
good_list = []
good_list_debug = []
for g_key in good_list_tmp:
for t_val in good_list_tmp[g_key]:
tmp_val = [-1] * len(full_key)
for f_ind, f_key in enumerate(full_key):
if f_key in g_key:
tmp_val[f_ind] = t_val[g_key.index(f_key)]
good_list.append(tmp_val)
good_list_debug.append([t_val, g_key])
return good_list, good_list_debug, full_three
def first_step(good_list, good_list_debug, expression_list, full_key, num_set, num_core):
good_list_split = []
size = int(len(good_list) / num_set)
if size == 0:
size = 1
while size < 3000 and size < len(good_list):
size *= 2
if size > 3000:
split_i = 0
print(len(good_list), len(good_list_debug))
while split_i < len(good_list):
#print(split_i, split_i+size)
good_list_split.append([good_list[split_i:split_i+size], good_list_debug[split_i:split_i+size],
full_key, expression_list])
split_i += size
num_core_step = len(good_list_split)
if num_core_step > num_core:
num_core_step = num_core
with Pool(num_core_step) as pool:
pool_return = pool.map(exclude_first, good_list_split)
good_list = []
good_list_debug = []
for pool_ret in pool_return:
if not pool_ret[0]:
break
for pool_ret_0 in pool_ret[0]:
good_list.append(pool_ret_0)
for pool_ret_1 in pool_ret[1]:
good_list_debug.append(pool_ret_1)
del pool_return
else:
good_list, good_list_debug = exclude_first([good_list, good_list_debug, full_key, expression_list])
return good_list, good_list_debug
def get_threes_analyze_part(args):
good_list_debug = args[0]
full_three = args[1]
threes_analyze = []
for _ in full_three:
threes_analyze.append(0)
for val, key in good_list_debug:
index_t = full_three.index(key)
if threes_analyze[index_t] == 0:
threes_analyze[index_t] = []
if val not in threes_analyze[index_t]:
threes_analyze[index_t].append(val)
print("threes_analyze ready")
for index, key in enumerate(full_three):
if threes_analyze[index] == 0:
continue
if len(threes_analyze[index]) == 0:
print("Key is missing. No solution", key)
return False
return threes_analyze
def get_threes_analyze(good_list_debug, full_three, num_set, num_core):
good_list_debug_split = []
size = int(len(good_list_debug) / num_set)
if size == 0:
size = 1
while size != 0 and size < 3000 and size < len(good_list_debug):
size *= 2
if size < len(good_list_debug):
split_i = 0
while split_i < len(good_list_debug):
good_list_debug_split.append([good_list_debug[split_i:split_i+size], full_three])
split_i += size
num_core_threes = len(good_list_debug_split)
if num_core_threes > num_core:
num_core_threes = num_core
with Pool(num_core_threes) as pool:
pool_return = pool.map(get_threes_analyze_part, good_list_debug_split)
threes_analyze = []
for _ in full_three:
threes_analyze.append([])
for pool_ret in pool_return:
for pool_ret_indx, pool_ret_val in enumerate(pool_ret):
if pool_ret_val == 0:
continue
#print(pool_ret_val)
if len(threes_analyze[pool_ret_indx]) > 0:
#for pool_ret_v in threes_analyze[pool_ret_indx]:
# if pool_ret_v not in pool_ret_val:
threes_analyze[pool_ret_indx].extend(pool_ret_val)
else:
threes_analyze[pool_ret_indx] = pool_ret_val
del pool_return
else:
threes_analyze = get_threes_analyze_part([good_list_debug, full_three])
for index, key in enumerate(full_three):
if threes_analyze[index] == 0:
print("No solution", key)
return False
return threes_analyze
def do_clean(threes_analyze, full_three, full_key, num_core, num_set):
full_indexes_to_index = {}
full_three_to_indexes = []
for indx, three_i in enumerate(full_three):
full_indexes_to_index[(full_key.index(three_i[0]), full_key.index(three_i[1]), full_key.index(three_i[2]))] = indx
full_three_to_indexes.append((full_key.index(three_i[0]), full_key.index(three_i[1]), full_key.index(three_i[2])))
for i in range(0, len(full_key)):
print("Cleaning step", i)
full_three_split = []
size = int(len(full_three) / num_set)
if size == 0:
size = 1
while size < 500 and size < len(full_three):
size *= 2
if size < len(full_three):
split_i = 0
while split_i < len(full_three):
full_three_split.append([full_three[split_i:split_i+size], threes_analyze, split_i,
full_key, full_indexes_to_index, full_three_to_indexes])
split_i += size
num_core_clean = len(full_three_split)
if num_core_clean > num_core:
num_core_clean = num_core
with Pool(num_core_clean) as pool:
pool_return = pool.map(clean_threes, full_three_split)
for pool_ret in pool_return:
if pool_ret == -1:
print("No solution")
return False
for pool_ret in pool_return:
if pool_ret:
break
else:
print("Cleaning finished")
break
for pool_ret in pool_return:
if not isinstance(pool_ret, bool):
start = pool_ret[1]
for threes_tmp in pool_ret[0]:
threes_analyze[start] = threes_tmp
start += 1
else:
was_not_in = False
counter_clean = 0
#print(threes_analyze)
for index_t, three in enumerate(full_three):
val_to_remove = []
for val in threes_analyze[index_t]:
val_to_rem = clean_three([val, threes_analyze, full_key, full_indexes_to_index,
full_three_to_indexes[index_t]])
if val_to_rem:
val_to_remove.append(val_to_rem)
for val in val_to_remove:
threes_analyze[index_t].remove(val)
if len(threes_analyze[index_t]) == 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("Cleaning finished")
break
return True
def find_solution(clause_number, args_dict, quick=False, num_set=8, num_core=8):
full_key = list(args_dict.keys())
full_key.sort()
print(full_key)
display_clause(clause_number)
expression_list, assignment_excluded = get_expression_list(clause_number, full_key)
good_list, good_list_debug, full_three = get_good_and_debug(full_key)
print("Arguments", full_key)
print("Length of list before exclude", len(good_list))
print("Expresion list", expression_list, len(expression_list))
good_list, good_list_debug = first_step(good_list, good_list_debug, expression_list, full_key, num_set, num_core)
print("Len after first step", len(good_list))
threes_analyze = get_threes_analyze(good_list_debug, full_three, num_set, num_core)
if threes_analyze is False:
return False
clean_status = do_clean(threes_analyze, full_three, full_key, num_core, num_set)
if not clean_status:
return False
if quick:
return True
# print("Good three list clean")
# for three in threes_analyze:
# print(three, threes_analyze[three])
# print("----")
final_good_first = [-1] * len(full_key)
first_three = (full_key[0], full_key[1], full_key[2])
first_three_val = threes_analyze[0][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, full_three)
print("Full key", full_key)
print("Final good:", final_good)
if not calculate_real_clause_list(clause_number, full_key, final_good):
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)
if len(clauses) == 0:
return True
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, full_three):
print("check tmp ", tmp_final_good)
for three_i, three_c in enumerate(full_three):
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_i]:
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_i])
return False
return True
def check_final_candidates(counter_minuses, tmp_final_good, full_key, clause_number):
if len(counter_minuses) == 3:
print(counter_minuses)
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[counter_minuses[0]] = last_vals[0]
tmp_final_last[counter_minuses[1]] = last_vals[1]
tmp_final_last[counter_minuses[2]] = last_vals[2]
print(tmp_final_last)
if not calculate_real_clause_list(clause_number, full_key, tmp_final_last):
print("Final candidate value does not solve the 3-SAT expression")
continue
return tmp_final_last
else:
print("No assignment. Should be")
exit(1)
if len(counter_minuses) == 2:
for last_vals in [[0, 0], [0, 1], [1, 0], [1, 1]]:
tmp_final_last = copy.deepcopy(tmp_final_good)
tmp_final_last[counter_minuses[0]] = last_vals[0]
tmp_final_last[counter_minuses[1]] = last_vals[1]
print(tmp_final_last)
if not calculate_real_clause_list(clause_number, full_key, tmp_final_last):
print("Final candidate value does not solve the 3-SAT expression")
continue
return tmp_final_last
else:
print("No assignment. Should be")
exit(1)
if len(counter_minuses) == 1:
print(counter_minuses)
for last_vals in [[0], [1]]:
tmp_final_last = copy.deepcopy(tmp_final_good)
tmp_final_last[counter_minuses[0]] = last_vals[0]
print(tmp_final_last)
if not calculate_real_clause_list(clause_number, full_key, tmp_final_last):
print("Final candidate value does not solve the 3-SAT expression")
continue
return tmp_final_last
else:
print("No assignment. Should be")
exit(1)
else:
print("Only one solution exist")
return tmp_final_good
def find_final(tmp_final_good, first_three, threes_analyze, full_key, assignment_excluded, clause_number, full_three):
print("First three", first_three)
for key in full_key[3:]:
candidates = []
current_three = (first_three[0], first_three[1], key)
for val in threes_analyze[full_three.index(current_three)]:
if val[0] == tmp_final_good[0] and val[1] == tmp_final_good[1]:
candidates.append(val[2])
if len(candidates) == 1:
tmp_final_good[full_key.index(key)] = candidates[0]
for key in full_key[3:]:
print('key no', key)
if tmp_final_good[full_key.index(key)] != -1:
continue
current_three = (first_three[0], first_three[1], key)
counter_minuses = []
for val_indx, val_tmp in enumerate(tmp_final_good):
if val_tmp == -1:
counter_minuses.append(val_indx)
if len(counter_minuses) <= 3:
return check_final_candidates(counter_minuses, tmp_final_good, full_key, clause_number)
candidates = []
for val in threes_analyze[full_three.index(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:
continue
else:
is_good_0 = False
tmp_final = copy.deepcopy(tmp_final_good)
print("Run for ", tmp_final, current_three, current_three, candidates[0])
tmp_final[full_key.index(key)] = candidates[0]
if check_tmp_final(tmp_final, threes_analyze, full_key, full_three):
if check_if_good(tmp_final, full_key, assignment_excluded):
tmp_final_good = tmp_final
print("Is good", tmp_final)
is_good_0 = True
if not is_good_0:
tmp_final_good[full_key.index(key)] = candidates[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 get_args():
parser = argparse.ArgumentParser(
prog='3sat solver',
description='Program solves 3sat problem'
)
parser.add_argument('-f ', '--filename', type=str, default="", help='3sat expression in cnf format')
parser.add_argument('-c ', '--count', type=int, default=30, help='Get number of arguments in expression')
parser.add_argument('-n', '--num_core', type=int, default=8, help='Number of cores')
parser.add_argument('-s', '--num_set', type=int, default=8, help='Number of set')
args = parser.parse_args()
print("Arguments", args.filename, args.count, args.num_core, args.num_set)
return args
def get_args_dict(count):
args_dict = {}
#for var in ["a", "b"]:]
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', 'm', 'n', 'o']:
for i in range(0, 20):
#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
if len(args_dict) == count:
return args_dict
def main():
arguments = get_args()
args_dict = get_args_dict(arguments.count)
if arguments.filename:
expression = parse_cnf(args_dict, arguments.filename)
else:
expression = gen_3sat_clause(args_dict, 205) # 45)
print("Expression", expression)
#number_real = test_3sat_real(expression, args_dict)
number_real = []
find_solution(expression, args_dict, num_set=arguments.num_set-1, num_core=arguments.num_core)
if __name__ == "__main__":
main()