Check is 2-CNF boolean function satisfiable, Using Resolution Method?

Question

The input is a Boolean formula in 2-CNF, given as a string of symbols.

Example: p /\ (p -> q) /\ (p -> ~r) /\ (~r / ~s) /\ (s / ~q)

I am using Resolution method to solve this 2 cnf sat problem but I am stuck with how to compare literals of two clauses in python as we need to check the variable and its negation in another clause

Answer 1

This is your homework, so no one is going to just do it for you. We can help if you're stuck at a specific point, but we won't do the work you are expected to do.

That said, I can give you some hints on how your code should be organized:

• First, split the input string in the variuos clauses
• Then you may want to transform the implications in disjunctions (you know the rule, don't you)
• At this point there are quite a few known algorithms, and I don't know what your teacher expects you to do. Let's say we adopt the simplest solution: generate all possible truth assignment for your variables, and check the resulting truth value for each clause. Note that you're working with a conjunction, so as soon as one clause is false the whole CNF is false

EDIT

Sorry for misunderstanding your question. simpy has a logic module with a lot of features, including a resolution function. But if you need to restrict yourself to the standard library then you will have to work a bit with strings.

I'm assuming each clause is: a) a single literal; b) an implication with exactly two literals; c) a disjunction of two or more literals, and that each variable is exactly 1 character. If we wanted to manage more complex cases we would need to define a simple tokenizer.

This is a possible code for the first function:

def is_sat(cnf):
    str_clauses = cnf.translate(str.maketrans("", "", "() ")).split("/\\")
    vars = {x for x in cnf if x in "abcdefghijklmnopqrstuvwxyz"}
    clauses = []
    for str_clause in str_clauses:
        if "->" in str_clause: ## <lit1 -> lit2>
            a,b = str_clause.split("->")
            clauses.append(set((negate(a), b)))
        elif "/" in str_clause: ## <lit1 / ... / litn>
            clauses.append(set(str_clause.split("/")))
        else: ##<lit1>
            clauses.append(set([str_clause]))
    for var in vars:
        ##remove tautologies
        tautology = set((var, negate(var)))
        for i,clause in enumerate(clauses[:]):
            if tautology == clause:
                del clauses[i]
            elif tautology < clause:
                clause -= tautology
        if not clauses:
            return True
        ##resolutions
        asserting = [i for i,c in enumerate(clauses) if var in c]
        negating = [i for i,c in enumerate(clauses) if negate(var) in c]
        while asserting and negating:
            if asserting[-1] > negating[-1]:
                x, y = asserting[-1], negating[-1]
                del asserting[-1]
                del negating[-1]
            else:
                y, x = asserting[-1], negating[-1]
                del negating[-1]
                del asserting[-1]
            resolved = (clauses[x] | clauses[y]) - tautology
            if not resolved:
                return False
            print(f'resolution: {clauses[x]}, {clauses[y]} => {resolved}')
            del clauses[x]
            del clauses[y]
            clauses.append(resolved)
    else:
        return True

def negate(s):
    if s[0] == '~':
        return s[1:]
    else:
        return '~' + s