加入收藏 | 设为首页 | 会员中心 | 我要投稿 李大同 (https://www.lidatong.com.cn/)- 科技、建站、经验、云计算、5G、大数据,站长网!
当前位置: 首页 > 百科 > 正文

在C中将逻辑公式转换为合数范式

发布时间:2020-12-16 10:00:54 所属栏目:百科 来源:网络整理
导读:我将使用Boots / Spirit在C中实现CNF生成器.但在完成“优先顺序”和“消除等价和含义”这两部分之后,我无法弄清楚如何实现“向内移动NOT”和“在ANDs上向ORs内部分配OR”. 此处记录了所需的输出: https://en.wikipedia.org/wiki/Conjunctive_normal_form 以
我将使用Boots / Spirit在C中实现CNF生成器.但在完成“优先顺序”和“消除等价和含义”这两部分之后,我无法弄清楚如何实现“向内移动NOT”和“在ANDs上向ORs内部分配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.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,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,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,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 inputn";
      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

解决方法

在向AND分配OR之前,应该向内移动:

!(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 OR X)

(A ornot(非B或C))和(不是A或(不是B或C))==>
(A或(不是B和notC))和(不是A或(不是B或C))==>
(Aor(B而不是C))和(不是A或不是B或C)==>
((AorB)和(Aornot C))和(不是A或不是B或C)==>
(A或B)和(A或非C)和(不是A或不是B或C)

也许我误解了你的问题并且你已经理解了所有上述转换,并且你在你创建的结构中执行该操作的机制有问题.

通过尝试完成打印例程中的所有转换,你当然已经为自己(可能是不可能的)做了很多事情.我会解析,然后转换,然后打印.

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

你有过:

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

但是你无法从iff一路递归l或r,并且在递归到达底部之前你不能直接生成任何“不”或“或”文本.因此,在打印时转换错误的设计,iff例程需要生成表示(l或不r)的临时对象,然后调用或处理例程来处理它,然后输出“AND”然后创建一个临时对象表示(不是l或r)并调用或处理例程来处理它.

类似地,或处理例程需要查看每个操作数.如果每个都只是最终变量的最终变量,或者只是将自己发送到流中.但是如果任何操作数更复杂,或者必须做一些更复杂的事情.

除了在开始打印之前进行转换之外,还可以更改其他一些内容以使代码更简单:

首先,你可以避免很多麻烦,或者和对象各自持有一个std :: set的任意数量的操作数,而不是一对操作数.这个代价很高,你需要一个适合对象的比较函数.但是,回报是值得拥有比较功能的麻烦.
接下来,您可能会考虑为所有子表达式使用单一类型,而不是为每个运算符指定一个类型.因此每个对象必须存储一个运算符和一组std ::操作数.这种设计选择存在一些非常大而明显的缺点,但有一个很大的优点:子表达式可以将自身转换为另一种类型.

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

这个语法的另一个好选择是在解析时进行所有转换.更复杂的问题确实值得完全拆分解析,转换,打印.但是在这种情况下,如果您通过工厂函数思考,转换非常适合解析:

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

> AND:

> a)两个输入都是AND,形成他们的集合的联合.
> b)一个输入是AND,将另一个输入插入到该组中.
> c)两个输入都不是AND,用这两个输入创建一个新的AND.

>或者:

> a)两个输入都是OR,形成了它们的集合.
> b)一个输入是OR,另一个是原始或NOT,将另一个输入插入OR的集合.
> c)至少有一个输入是AND,在AND上分配另一个输入(分配函数必须处理丑陋的子情况).

>不是:

>原始的倒置是微不足道的. NOT的反转是微不足道的. OR的反转非常简单. AND的反转是整个设计中最丑陋的东西(你需要将整个内容全部转出来)但是可行.为了保持理智,你可能会忘记效率并递归地使用工厂来进行NOT和OR操作,这些操作是NOT和平凡转换的(但是需要进一步转换才能返回到CNF).

> IFF和IMP:只需对基本工厂进行适当的多次调用.

(编辑:李大同)

【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容!

    推荐文章
      热点阅读