Plans for literals ("concrete")
More...
Go to the source code of this file.
Detailed Description
Plans for literals ("concrete")
 Todo:
 Boolean literals, and more general literals

We have a notion of "boolean variables" and "boolean literals" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac; seems sufficient, and needs documentation.

The universal set of values is {false,true}.

Given a boolean literal x, the associated condition is
lambda([f], is(f(v) = is(x > 0)))

A "monosigned literal" is a pair [v,e], where v is the variable (just a symbol) and e the value.

var_m([v,e]) = v and val_m([v,e]) = e.

Interpreted as a CNFliteral (a "negative monosigned literal"), the associated condition is
lambda([f], is(f(v) # e))
while for a DNFliteral (a "positive monosigned literal") we have lambda([f], is(f(v) = e))

A "signed literal" is a pair [v,S], where S is a set of values.

var_s([v,S]) = v and val_s([v,S]) = S.

For a "negative signed literal" (CNFliteral) the associated condition is
lambda([f], not elementp(f(v), S))
while for the "positive signed literal" (DNFliteral) it is lambda([f], elementp(f(v), S))

We need to provide the standard promotion of literals (to more general literals).

Compare "Domain association and allowed total assignments" in ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp.

DONE (we use concrete representations, exactly as in the mathematical definition) Perhaps there is a third entry? With tags? No.
Definition in file Literals.hpp.