Блог

Входные данные представляют собой логическую формулу в 2-CNF, заданную в виде строки символов.

Пример: p / (p -> q) / (p ->> ~r) / (~r / ~s) / (s / ~q)

Я использую метод разрешения для решения этой проблемы 2 cnf sat, но я застрял в том, как сравнивать литералы двух предложений в python, так как нам нужно проверить переменную и ее отрицание в другом предложении

Это твоя домашняя работа, так что никто не собирается просто делать это за тебя. Мы можем помочь, если вы застряли в определенной точке, но мы не будем выполнять ту работу, которую от вас ожидают.

Тем не менее, я могу дать вам несколько советов о том, как должен быть организован ваш код:

• Во-первых, разделите входную строку в предложениях variuos
• Тогда вы, возможно, захотите преобразовать последствия в дизъюнкции (вы знаете правило, не так ли).
• На данный момент существует довольно много известных алгоритмов, и я не знаю, чего ожидает от вас ваш учитель. Предположим, мы примем самое простое решение: сгенерируем все возможные значения истинности для ваших переменных и проверим полученное значение истинности для каждого предложения. Обратите внимание, что вы работаете с конъюнкцией, поэтому, как только одно предложение является ложным, весь CNF является ложным

Редактировать

Извините, что неправильно понял ваш вопрос. simpy имеет logic модуль с множеством функций, включая функцию разрешения. Но если вам нужно ограничиться стандартной библиотекой, вам придется немного поработать со строками.

Я предполагаю, что каждое предложение представляет собой: а) один литерал; б) импликацию с ровно двумя литералами; в) дизъюнкцию двух или более литералов и что каждая переменная имеет ровно 1 символ. Если бы мы хотели управлять более сложными случаями, нам нужно было бы определить простой токенизатор.

Это возможный код для первой функции:

 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