CNF (Conjunctive Normal Form)

check-cnf.js

var cnfs = [
  // (a || c) && (c || d || b)
  new Term(
    Term.AND,
    new Term(
      Term.OR,
      new Term(Term.LITERAL, "a"),
      new Term(Term.LITERAL, "c")
    ),
    new Term(
      Term.OR,
      new Term(
        Term.OR,
        new Term(Term.LITERAL, "c"),
        new Term(Term.LITERAL, "d")
      )
      ,
      new Term(Term.LITERAL, "b")
    )
  )
];

// not CNF
var nonCnfs = [
  // !(b || c)
  new Term(
    Term.OR,
    new Term(Term.LITERAL, "b"),
    new Term(Term.LITERAL, "c")
  ).negate(),
  // (a && b) || c
  new Term(
    Term.OR,
    new Term(
      Term.AND,
      new Term(Term.LITERAL, "a"),
      new Term(Term.LITERAL, "b")
    ),
    new Term(Term.LITERAL, "c")
  ),
  // a && (b || (d && e))
  new Term(
    Term.AND,
    new Term(Term.LITERAL, "a"),
    new Term(
      Term.OR,
      new Term(Term.LITERAL, "b"),
      new Term(
        Term.AND,
        new Term(Term.LITERAL, "d"),
        new Term(Term.LITERAL, "e")
      )
    )
  )
];

function checkCNF(form) {
  console.log("--------------------------------------------------");
  console.log("ORIGINAL       | " + form.toString());
  console.log("SHOVE NEGATION | " + form.shoveNegation().toString());
  console.log("CNF            | " + form.toCNF().toString());
}

console.log("\n*** CNFs ***\n");
cnfs.forEach(checkCNF);
console.log("\n*** Non-CNFs ***\n");
nonCnfs.forEach(checkCNF);

cnf.js

function Term(type) {
  this.type = type;
  this.negated = false;

  switch (type) {
  case Term.AND:
  case Term.OR:
    this.left  = arguments[1];
    this.right = arguments[2];
    break;
  case Term.LITERAL:
    this.literal = arguments[1];
    break;
  }
}

Term.AND     = " && ",
Term.OR      = " || ",
Term.LITERAL = " LITERAL ";

Term.prototype.negate = function () {
  this.negated = !this.negated;
  return this;
};

Term.prototype.deMorgen = function () {
  if (this.hasChildren()) {
    this.negate();
    this.type = this.oppositeType();
    this.left.negate();
    this.right.negate();
  }

  return this;
};

Term.prototype.shoveNegation = function () {
  // top-down
  if (this.negated)
    this.deMorgen();

  if (this.hasChildren()) {
    this.left.shoveNegation();
    this.right.shoveNegation();
  }

  return this;
};

Term.prototype.distributeDisjunction = function () {
  // bottom-up
  if (this.hasChildren()) {
    this.left.distributeDisjunction();
    this.right.distributeDisjunction();
  }

  if (this.type == Term.OR) {
    // (Q && R) || P -> (Q || P) && (R || P)

    var decomposeTarget;        // (Q && R)
    var injectTarget;           // P

    if (this.left.type == Term.AND) {
      decomposeTarget = this.left;
      injectTarget    = this.right;
    } else if (this.right.type == Term.AND) {
      decomposeTarget = this.right;
      injectTarget    = this.left;
    } else {
      // nothing to do
      return this;
    }

    // (Q || P)
    var newLeft = injectTarget.equalTo(decomposeTarget.left)
          ? injectTarget
          : new Term(
            Term.OR,
            decomposeTarget.left,     // Q
            injectTarget              // P
          );

    // (R || P)
    var newRight = injectTarget.equalTo(decomposeTarget.right)
          ? injectTarget
          : new Term(
            Term.OR,
            decomposeTarget.right,    // R
            injectTarget              // P
          );

    this.type  = Term.AND;
    this.left  = newLeft;
    this.right = newRight;
  }

  return this;
};

Term.prototype.toCNF = function () {
  this.shoveNegation();
  this.distributeDisjunction();
  return this;
};

Term.prototype.oppositeType = function () {
  return this.type == Term.AND ? Term.OR : Term.AND;
};

Term.prototype.hasChildren = function () {
  return this.type != Term.LITERAL;
};

// deeply compare
Term.prototype.equalTo = function (term) {
  if (this.type != term.type)
    return false;

  if (this.type == Term.LITERAL)
    return this.literal == term.literal;

  return this.type == term.type &&
    this.left.equalTo(term.left) &&
    this.right.equalTo(term.right);
};

Term.prototype.toString = function () {
  return this.stringExpression(this.type);
};

Term.prototype.stringExpression = function (parentType) {
  var str;

  switch (this.type) {
  case Term.LITERAL:
    str = this.literal;
    break;
  case Term.AND:
  case Term.OR:
    str =
      this.left.stringExpression(this.type) +
      this.type +
      this.right.stringExpression(this.type);
    if (this.negated || this.type != parentType)
      str = "(" + str + ")";
    break;
  }

  return (this.negated ? "!" : "") + str;
};

result.txt

*** CNFs ***

--------------------------------------------------
ORIGINAL       | (a || c) && (c || d || b)
SHOVE NEGATION | (a || c) && (c || d || b)
CNF            | (a || c) && (c || d || b)

*** Non-CNFs ***

--------------------------------------------------
ORIGINAL       | !(b || c)
SHOVE NEGATION | !b && !c
CNF            | !b && !c
--------------------------------------------------
ORIGINAL       | (a && b) || c
SHOVE NEGATION | (a && b) || c
CNF            | (a || c) && (b || c)
--------------------------------------------------
ORIGINAL       | a && (b || (d && e))
SHOVE NEGATION | a && (b || (d && e))
CNF            | a && (d || b) && (e || b)