mlr3pipelines (version 0.7.0)

CnfAtom: Atoms for CNF Formulas

Description

CnfAtom objects represent a single statement that is used to build up CNF formulae. They are mostly intermediate, created using the %among% operator or CnfAtom() directly, and combined into CnfClause and CnfFormula objects. CnfClause and CnfFormula do not, however, contain CnfAtom objects directly,

CnfAtoms contain an indirect reference to a CnfSymbol by referencing its name and its CnfUniverse. They furthermore contain a set of values. An CnfAtom represents a statement asserting that the given symbol takes up one of the given values.

If the set of values is empty, the CnfAtom represents a contradiction (FALSE). If it is the full domain of the symbol, the CnfAtom represents a tautology (TRUE). These values can be converted to, and from, logical(1) values using as.logical() and as.CnfAtom().

CnfAtom objects can be negated using the ! operator, which will return the CnfAtom representing set membership in the complement of the symbol with respect to its domain. CnfAtoms can furthermore be combined using the | operator to form a CnfClause, and using the & operator to form a CnfFormula. This happens even if the resulting statement could be represented as a single CnfAtom.

This is part of the CNF representation tooling, which is currently considered experimental; it is for internal use.

Usage

CnfAtom(symbol, values)
e1 %among% e2
as.CnfAtom(x)

Value

A new CnfAtom object.

Arguments

symbol

(CnfSymbol)
The symbol to which the atom refers.

values

(character)
The values that the symbol can take.

e1

(CnfSymbol)
Left-hand side of the %among% operator. Passed as symbol to CnfAtom().

e2

(character)
Right-hand side of the %among% operator. Passed as values to CnfAtom().

x

(any)
The object to be coerced to a CnfAtom by as.CnfAtom. Only logical(1) and CnfAtom itself are currently supported.

Details

We would have preferred to overload the %in% operator, but this is currently not easily possible in R. We therefore created the %among% operator.

The internal representation of a CnfAtom may change in the future.

See Also

Other CNF representation objects: CnfClause(), CnfFormula(), CnfSymbol(), CnfUniverse()

Examples

u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))

CnfAtom(X, c("a", "b"))
X %among% "a"
X %among% character(0)
X %among% c("a", "b", "c")

as.logical(X %among% character(0))
as.CnfAtom(TRUE)

!(X %among% "a")

X %among% "a" | X %among% "b"  # creates a CnfClause

X %among% "a" & X %among% c("a", "b")  # creates a CnfFormula