OKlibrary  0.2.1.6
Literals.hpp File Reference

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.
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.