Literals.hpp File Reference

Plans for literals ("concrete") More...

Go to the source code of this file.

Detailed Description

Plans for literals ("concrete")

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.
    1. The universal set of values is {false,true}.
    2. 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.
    1. var_m([v,e]) = v and val_m([v,e]) = e.
    2. Interpreted as a CNF-literal (a "negative monosigned literal"), the associated condition is
      lambda([f], is(f(v) # e))
      while for a DNF-literal (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.
    1. var_s([v,S]) = v and val_s([v,S]) = S.
    2. For a "negative signed literal" (CNF-literal) the associated condition is
      lambda([f], not elementp(f(v), S))
      while for the "positive signed literal" (DNF-literal) 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.