Convert logic formula to conjunctive normal form in C++

Question

I'm going to implement a CNF generator in C++, using Boots/Spirit. but after finish "the order of precedence" and "eliminating equivalences & implications" these two parts, I can't figure out how to implement "move NOTs inwards" and "distribute ORs inwards over ANDs".

Desired output is documented here: https://en.wikipedia.org/wiki/Conjunctive_normal_form

Here are more detail description below:

The order of precedence:

NOT > AND > OR > IMP > IFF

Input example:

A iff B imp C

Now the output is:

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

And the code( I implement output at printer part ):

#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;
}

Compiling command:

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

Answer 1

Moving NOT inward should be done before distributing OR across AND:

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

remember to cancel any !!X that occurs while doing that.

Also drop redundant ( )

OR distributes across AND:

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

You Probably need to reduce some other redundancies that will creep in as you do all that, such as (X OR X)

(A ornot( not B or C)) and ( not A or ( not B or C)) ==>
(A or (notnot B andnotC)) and ( not A or(not B or C)) ==>
(Aor( B and not C)) and ( not A or not B or C) ==>
((​AorB) and (Aornot 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)

Maybe I misunderstood your question and you already understood all the above transformations, and you are having trouble with the mechanics of doing that inside the structure you have created.

You certainly have made things hard for yourself (maybe impossible) by trying to accomplish all the transformations inside the print routine. I would have parsed, then transformed, then printed.

If you insist on transforming in the print routine, then you likely miss some simplifications and you need print to be more aware of the rules of CNF. An AND node can simply print its two sides recursively with AND in between. But any other node most first inspect its children and conditionally transform enough to pull an AND up to the top before recursively calling.

You had:

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 << ")";
}

But you can't recurse all the way into l or r from iff and you can't directly generate any "not" or "or" text until you have recursively reached the bottom. So with the mis design of transforming while printing, the iff routine would need to generate a temp object representing (l or not r) and then call the or processing routine to handle it, then output "AND" then create a temp object representing (not l or r) and call the or processing routine to handle it.

Similarly, the or processing routine would need to look at each operand. If each is simply a final variable or not of a final variable, or can simply emit itself to the stream. But if any operand is more complicated, or must do something more complicated.

In addition to doing transformation before you start printing, there are a couple other things you might change in order to make the code simpler:

First, you could avoid a lot of trouble by having or and and objects each hold a std::set of any number of operands, rather than a pair of operands. The big cost of that is you need a decent comparison function for the objects. But the pay back is worth the trouble of having a comparison function. Next, you might consider having a single type for all subexpressions, rather than having a type for each operator. So each object must store an operator and a std::set of operands. There are some pretty big and obvious disadvantages to that design choice, but there is one big advantage: A subexpression can transform itself into a different kind.

The more common subexpression transformation scheme (which might still be best, just consider alternatives) is for the owner of a subexpression to ask the subexpression to conditionally generate a transformed clone of itself. That is more efficient than having objects able to directly transform themselves. But getting the coding details right requires more thought.

Another good choice for this grammar is to do all the transformations while parsing. More complicated problems really deserve the full split of parse, transform, print. But in this case transform fits beautifully into parsing if you think through your factory function:

The factory takes an operator and one (for NOT) or two subexpressions that are already CNF. It produces a new CNF expression:

• AND:

  • a) Both inputs are AND's, form the union of their sets.
  • b) One input is an AND, insert the other input into that one's set.
  • c) Neither input is an AND, create a new AND with those two inputs.

• OR:

  • a) Both inputs are OR's, form the union of their sets.
  • b) One input is an OR and the other is primitive or NOT, insert the other input into the OR's set.
  • c) At least one input is an AND, distribute the other input across that AND (the distribute function must handle the ugly sub cases).

• NOT:

  • Inversion of a primitive is trivial. Inversion of a NOT is trivial. Inversion of an OR is pretty trivial. Inversion of an AND is the ugliest thing in this whole design (you need to turn the whole thing inside out) but is doable. To keep your sanity, you could forget about efficiency and use the factory recursively for the NOT and OR operations that a NOT AND trivially transforms to (but which need further transformation to get back to CNF).
• IFF and IMP: Just make the appropriate several calls to the basic factories.