Any Boolean satisfiability problem can be rewritten in the form of distinct sections of variables containing or and and functions between them. The individual variables can be negated with not wherever needed in this form, called a conjunctive normal form. We can further rewrite any expression in this form to contain at most three variables in each section, which will be useful in algorithmic analysis (dummy variables otherwise not used can be introduced to help). This is done to simplify the algorithmic analysis. For example, the following is a Boolean expression over four variables in the conjunctive normal form restricted to three variables per section:
(not a or b or d) and \
(not b or c or d) and \
(a or not c or d) and \
(not a or not b or not d) and \
(b or not c or not d) and \
(not a or c or not d) and \
(a or b or c) and \
(not a or not b or not c)
The Boolean satisfiability problem (SAT) associated with this expression would ask whether there is any combination of a, b, c, and d values for which the expression evaluates to true. Since we've restricted our sections to contain at most three variables, this variation of the Boolean satisfiability problem is known as 3SAT.
Now, we can write a function to determine whether the Boolean expression given before is satisfiable:
def checker(f,candidate):
"""
f: can be any function which takes as a string of 1s and 0s which is at least as long as the number of variables in f. Right most character is the 0th bit.
candidate: should be a string of 1s and 0s which is at least as long as the number of variables in f. Right most character is the 0th bit.
"""
return(f(candidate))
def try_all_inputs(f,len_input):
import itertools
result=[]
for candidate in ["".join(seq) for seq in itertools.product("01", repeat=len_input)]:
if checker(f,candidate):
result+=[candidate]
return result # list of inputs which the function
# f validates to true
def is_satisfiable(f,len_input):
return len(try_all_inputs(f,len_input))>0
def a_3sat_function_4(binary_string):
"""
binary_string is a string that is at least 4 characters long with 1s and 0s with the rightmost character representing the 0th bit
"""
binary_list=[int(i) for i in binary_string]
binary_list.reverse()
a,b,c,d=binary_list[0:4]
return (not a or b or d) and \
(not b or c or d) and \
(a or not c or d) and \
(not a or not b or not d) and \
(b or not c or not d) and \
(not a or c or not d) and \
(a or b or c) and \
(not a or not b or not c)
Using the previous code, we can see if our function a_3sat_function is satisfiable, and get a list of all possible inputs which satisfy it with the following code:
print(is_satisfiable(a_3sat_function_4,4))
print(try_all_inputs(a_3sat_function_4,4))
With the previous code, we see that a_3sat_function is satisfiable and the inputs which satisfy it are 1010 and 1110 as the following is printed:
True ['1010', '1110']