Closed adrianperezkeilty closed 9 months ago
Interesting question. I haven't thought about it in a while.
Here's the code that checks if an expression is a CNF/DNF:
bool
BX_IsDNF(struct BoolExpr *ex)
{
if (BX_IS_ZERO(ex) || BX_IS_LIT(ex))
return true;
if (BX_IS_OR(ex)) {
for (size_t i = 0; i < ex->data.xs->length; ++i) {
struct BoolExpr *x = ex->data.xs->items[i];
if (!BX_IS_LIT(x) && !(BX_IS_AND(x) && _bx_is_clause(x)))
return false;
}
return true;
}
if (BX_IS_AND(ex))
return _bx_is_clause(ex);
return false;
}
bool
BX_IsCNF(struct BoolExpr *ex)
{
if (BX_IS_ONE(ex) || BX_IS_LIT(ex))
return true;
if (BX_IS_OR(ex))
return _bx_is_clause(ex);
if (BX_IS_AND(ex)) {
for (size_t i = 0; i < ex->data.xs->length; ++i) {
struct BoolExpr *x = ex->data.xs->items[i];
if (!BX_IS_LIT(x) && !(BX_IS_OR(x) && _bx_is_clause(x)))
return false;
}
return true;
}
return false;
}
IIRC, the answer to your question relates to whether a DNF or CNF can be represented in a simplified form. Here are a few valid CNFs:
1
(-1, 2, -3, 4)
((-1, 2), (-3, 4))
But what does ()
represent? Since the identity of the AND
function is True
, an "empty" CNF must be True
. Therefore True
is a valid CNF - the empty CNF. Likewise, False
is a valid DNF - the empty DNF.
So then how do you represent False
as a CNF? Only indirectly by specifying an unsatisfiable CNF, like ((-1, ), (1, ))
. It has no direct representation.
Most of this is related to defining data structures for algorithmic manipulation. In this case a CNF representation is used by SAT, and a DNF representation (implicant table) is used by Espresso.
So a CNF/DNF is really a data structure. And it's not correct that the data structure can represent either Zero or One.
Good question, but I don't see a need to change this.
I've noticed that the expressions Zero and One have the fixed forms DNF and CNF respectively and cannot be changed:
I'd like to input several expressions to the espresso minimization algorithm
espresso_exprs
for efficiency purposes but in some cases an expression may be reduced to One which will result in a"expected a DNF expression"
error:Why can't the normal forms of Zero and One be flipped since they can be seen both as either DNF or CNF?