Решение булевых выражений с использованием прямого цепочки

Question

Может ли кто-нибудь помочь мне с решением булевых выражений с помощью форвардной цепочки. Хороший учебник также поможет мне.

Пример: A.(A + B) = A

A.(A + B) => A.A + A.B [Применение дистрибутивный закон]

A.A + A.B => A + A.B [Применение идемпотентность закон]

A + A.B => A.(1 + B)

A.(1 + B) => A.(1) => A

Я сделал огромные усилия, но до сих пор не могу этого сделать. Процедура потребует разбора булевого выражения, а затем проверки рекурсивного правила. Я думал о создании двоичного дерева выражения, а затем выполнял проверку правил. Правильно ли мой подход? Если нет, предложите мне альтернативу.

Answer 1

Одним из подходов к решению проблемы может быть использование метода грубой силы. Под этим я имею в виду: попробуйте каждую возможную комбинацию значений A и B (или сколько бы у вас значений) и генерируйте таблицу истинности результатов.

Следующий пример иллюстрирует это (хотя он больше в стиле C, а не C++).

#include <iostream> 
#include <algorithm> 
#include <cmath> 
#include <cassert> 

const unsigned g_unValues = 2; 

bool expression(int values[]) 
{ 
    return !!(values[0] * (values[0] + values[1])); 
} 

void truth_table(bool (*func)(int[]), unsigned nvalues); 

int main(int argc, char** argv) 
{ 
    truth_table(expression, g_unValues); 

    return 0; 
} 

void truth_table(bool (*func)(int[]), unsigned nvalues) 
{ 
    assert(pow(2, nvalues) <= sizeof(unsigned)); 

    int values[nvalues]; 
    unsigned individuals[nvalues]; 
    unsigned result = 0; 

    std::fill_n(individuals, nvalues, 0); 

    // Display truth table header 
    for (unsigned j = 0; j < nvalues; j++) std::cout << char('A'+j) << ' '; 
    std::cout << "| Result" << std::endl; 

    for (unsigned i = 1; i <= pow(2, nvalues); i++) 
    { 
     for (unsigned j = 0; j < nvalues; j++) 
     { 
      values[j] = i & 0x1<<j; 
      if (values[j]) individuals[j] |= 0x1<<i; 
     } 

     bool eval = func(values); 
     if (eval) result |= 0x1<<i; 

     // Display truth table entry 
     for (unsigned j = 0; j < nvalues; j++) std::cout << !!values[j] << ' '; 
     std::cout << "| " << eval << std::endl; 
    } 

    for (unsigned j = 0; j < nvalues; j++) 
    { 
     if (result != individuals[j]) continue; 
     std::cout << "Expression equivalence: " << char('A'+j) << std::endl; 
     break; 
    } 
} 

Этот код сам по себе не очень полезно, но это может дать вам некоторые идеи вы должны выбрать метод грубой силы. Вы можете адаптировать код для создания expression из строки, предоставленной пользователем. Для выражений, которые не упрощаются до одного вывода, вы можете заменить код, который сравнивает входные столбцы таблицы истинности с столбцом результата с методом генерации минимальной строки (упрощение начального входного логического выражения).

Надеюсь, это как-то полезным, удачи :)

Answer 2

я предполагаю, что C++ Prop библиотека (http://www.cs.nyu.edu/leunga/prop.html) может быть полезным для этого: она обеспечивает символический срок представления и переписывания поддержки, которая может быть использована для реализации системы