c++ - 将逻辑公式转换为C++中的合取范式

Question

我将使用Boots/Spirit在C++中实现CNF生成器。但是在完成了“优先顺序”和“消除对等与含意”这两部分之后，我无法弄清楚如何实现“向内移动NOT”和“向AND内分发OR”。

所需的输出记录在这里:
https://en.wikipedia.org/wiki/Conjunctive_normal_form

以下是更多详细说明:

优先顺序:

NOT > AND > OR > IMP > IFF

输入示例:

A iff B imp C

现在的输出是:

(A or not ( not B or C)) and ( not A or ( not B or C))

和代码(我在打印机部分实现输出):

#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
#include <boost/spirit/include/phoenix_operator.hpp>
#include <boost/variant/recursive_wrapper.hpp>

namespace qi    = boost::spirit::qi;
namespace phx   = boost::phoenix;



// Abstract data type

struct op_or  {};
struct op_and {};
struct op_imp {};
struct op_iff {};
struct op_not {};

typedef std::string var;
template <typename tag> struct binop;
template <typename tag> struct unop;

typedef boost::variant<var,
        boost::recursive_wrapper<unop <op_not> >,
        boost::recursive_wrapper<binop<op_and> >,
        boost::recursive_wrapper<binop<op_or> >,
        boost::recursive_wrapper<binop<op_imp> >,
        boost::recursive_wrapper<binop<op_iff> >
        > expr;

template <typename tag> struct binop
{
  explicit binop(const expr& l, const expr& r) : oper1(l), oper2(r) { }
  expr oper1, oper2;
};

template <typename tag> struct unop
{
  explicit unop(const expr& o) : oper1(o) { }
  expr oper1;
};



// Operating on the syntax tree

struct printer : boost::static_visitor<void>
{
  printer(std::ostream& os) : _os(os) {}
  std::ostream& _os;

  //
  void operator()(const var& v) const { _os << v; }

  void operator()(const binop<op_and>& b) const { print(" and ", b.oper1, b.oper2); }
  void operator()(const binop<op_or >& b) const { print(" or ", b.oper1, b.oper2); }
  void operator()(const binop<op_iff>& b) const { eliminate_iff(b.oper1, b.oper2); }
  void operator()(const binop<op_imp>& b) const { eliminate_imp(b.oper1, b.oper2); }

  void print(const std::string& op, const expr& l, const expr& r) const
  {
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << op;
    boost::apply_visitor(*this, r);
    _os << ")";
  }

  void operator()(const unop<op_not>& u) const
  {
    _os << "( not ";
    boost::apply_visitor(*this, u.oper1);
    _os << ")";
  }

  void eliminate_iff(const expr& l, const expr& r) const
  {
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << " or not ";
    boost::apply_visitor(*this, r);
    _os << ") and ( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
  }

  void eliminate_imp(const expr& l, const expr& r) const
  {
    _os << "( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
  }
};

std::ostream& operator<<(std::ostream& os, const expr& e)
{ boost::apply_visitor(printer(os), e); return os; }



// Grammar rules

template <typename It, typename Skipper = qi::space_type>
struct parser : qi::grammar<It, expr(), Skipper>
{
  parser() : parser::base_type(expr_)
  {
    using namespace qi;

    expr_  = iff_.alias();

    iff_ = (imp_ >> "iff" >> iff_) [ _val = phx::construct<binop<op_iff>>(_1, _2) ] | imp_   [ _val = _1 ];
    imp_ = (or_  >> "imp" >> imp_) [ _val = phx::construct<binop<op_imp>>(_1, _2) ] | or_    [ _val = _1 ];
    or_  = (and_ >> "or"  >> or_ ) [ _val = phx::construct<binop<op_or >>(_1, _2) ] | and_   [ _val = _1 ];
    and_ = (not_ >> "and" >> and_) [ _val = phx::construct<binop<op_and>>(_1, _2) ] | not_   [ _val = _1 ];
    not_ = ("not" > simple       ) [ _val = phx::construct<unop <op_not>>(_1)     ] | simple [ _val = _1 ];

    simple = (('(' > expr_ > ')') | var_);
    var_ = qi::lexeme[ +alpha ];

    BOOST_SPIRIT_DEBUG_NODE(expr_);
    BOOST_SPIRIT_DEBUG_NODE(iff_);
    BOOST_SPIRIT_DEBUG_NODE(imp_);
    BOOST_SPIRIT_DEBUG_NODE(or_);
    BOOST_SPIRIT_DEBUG_NODE(and_);
    BOOST_SPIRIT_DEBUG_NODE(not_);
    BOOST_SPIRIT_DEBUG_NODE(simple);
    BOOST_SPIRIT_DEBUG_NODE(var_);
  }

  private:
  qi::rule<It, var() , Skipper> var_;
  qi::rule<It, expr(), Skipper> not_, and_, or_, imp_, iff_, simple, expr_;
};




// Test some examples in main and check the order of precedence

int main()
{
  for (auto& input : std::list<std::string> {

      // Test the order of precedence
      "(a and b) imp ((c and d) or (a and b));",
      "a and b iff (c and d or a and b);",
      "a and b imp (c and d or a and b);",
      "not a or not b;",
      "a or b;",
      "not a and b;",
      "not (a and b);",
      "a or b or c;",
      "aaa imp bbb iff ccc;",
      "aaa iff bbb imp ccc;",


      // Test elimination of equivalences
      "a iff b;",
      "a iff b or c;",
      "a or b iff b;",
      "a iff b iff c;",

      // Test elimination of implications
      "p imp q;",
      "p imp not q;",
      "not p imp not q;",
      "p imp q and r;",
      "p imp q imp r;",
      })
  {
    auto f(std::begin(input)), l(std::end(input));
    parser<decltype(f)> p;

    try
    {
      expr result;
      bool ok = qi::phrase_parse(f,l,p > ';',qi::space,result);

      if (!ok)
        std::cerr << "invalid input\n";
      else
        std::cout << "result: " << result << "\n";

    } catch (const qi::expectation_failure<decltype(f)>& e)
    {
      std::cerr << "expectation_failure at '" << std::string(e.first, e.last) << "'\n";
    }

    if (f!=l) std::cerr << "unparsed: '" << std::string(f,l) << "'\n";
  }

  return 0;
}

编译命令:

clang++ -std=c++11 -stdlib=libc++ -Weverything CNF_generator.cpp

Answer 1

在AND之间分配OR之前，应先进行NOT向内移动:

!(A AND B) ==> (!A OR !B)
!(A OR B) ==> (!A AND !B)

切记取消执行此操作时发生的任何!!X。

同时删除多余的( )
或分布在AND之间:

A OR (B AND C) ==> (A OR B) AND (A OR C)

您可能需要减少执行这些操作时会蔓延的其他一些冗余，例如(X或X)
(A or not ( not B or C)) and ( not A or ( not B or C)) ==>(A or ( not not B and not C)) and ( not A or ( not B or C ) ) ==>(A or ( B and not C)) and ( not A or not B or C) ==> ( (A or B) and (A or not C) ) and ( not A or not B or C) ==>(A or B) and (A or not C) and ( not A or not B or C)
也许我误解了您的问题，并且您已经理解了上述所有转换，并且在创建的结构中执行该转换的机制遇到了麻烦。

通过尝试完成打印例程中的所有转换，您当然会使自己变得困难(可能是不可能的)。我本来会解析，然后转换，然后打印。

如果您坚持要在打印例程中进行转换，那么您可能会错过一些简化，您需要打印才能更加了解CNF的规则。 AND节点可以简单地递归地打印其两侧，而AND介于两者之间。但是，其他任何节点最先检查其子节点并有条件地进行转换，以在递归调用之前将AND拉到顶部。

你有过:

void eliminate_iff(const expr& l, const expr& r) const
{
    _os << "(";
    boost::apply_visitor(*this, l);
    _os << " or not ";
    boost::apply_visitor(*this, r);
    _os << ") and ( not ";
    boost::apply_visitor(*this, l);
    _os << " or ";
    boost::apply_visitor(*this, r);
    _os << ")";
}

但是您不能从iff一直递归到l或r中，并且除非递归到达底部，否则无法直接生成任何"not"或"or"文本。因此，由于在打印时进行转换的错误设计，iff例程将需要生成一个表示(l或不是r)的临时对象，然后调用or处理例程来处理它，然后输出"AND"然后创建一个表示(不是l的临时对象)或r)，然后调用or处理例程进行处理。

同样，or处理例程将需要查看每个操作数。如果每个仅是最终变量或最终变量的not，则or可以简单地将自身发送到流中。但是，如果任何操作数更复杂，则or必须执行更复杂的操作。

除了在开始打印之前进行转换之外，您还可以更改其他几项以便使代码更简单:

首先，通过让or和and对象每个都持有任意数量的操作数而不是一对操作数的std::set，可以避免很多麻烦。这样做的最大代价是您需要为对象提供不错的比较功能。但是投资返回值得拥有比较功能的麻烦。
接下来，您可以考虑为所有子表达式具有单一类型，而不是为每个运算符具有类型。因此，每个对象都必须存储一个运算符和一个操作数的std::set。该设计选择有很多明显的缺点，但是有一个很大的优点:子表达式可以将自身转换为另一种表达式。

较常见的子表达式转换方案(可能仍然是最好的，仅考虑替代方法)是子表达式的所有者要求子表达式有条件地生成自身的转换克隆。这比使对象能够直接转换自身更有效。但是正确编写编码细节需要更多的思考。

此语法的另一个不错的选择是在解析时进行所有转换。实际上，更复杂的问题应完全解析，转换和打印。但是在这种情况下，如果您通过工厂功能来考虑，则转换很适合解析:

工厂需要一个运算符和一个(对于NOT)或两个已经是CNF 的子表达式。它产生一个新的CNF表达式:

AND:

a)两个输入都是AND，形成它们集合的并集。

b)一个输入是一个AND，将另一个输入插入该输入的集合中。

c)两个输入都不是AND，使用这两个输入创建一个新的AND。

OR:

a)两个输入都是OR，形成它们集合的并集。

b)一个输入是OR，另一个输入是原始或NOT，将另一个输入插入OR的集合中。

c)至少一个输入是AND，将另一个输入分布在该AND上(distribution函数必须处理难看的子情况)。

NOT:

原语的反转很简单。 NOT的反转很简单。 OR的反转非常简单。在整个设计中，AND的反转是最丑陋的事情(您需要将整个内容从里到外)，但这是可行的。为了保持理智，您可能会忘记效率，而将工厂递归地用于NOT琐碎地转换为的OR和NOT AND操作(但是需要进一步转换才能返回到CNF)。

IFF和IMP:只需对基本工厂进行适当的几次调用即可。