CnfAtom: Atoms for CNF Formulas

In mlr3pipelines: Preprocessing Operators and Pipelines for 'mlr3'

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)

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.

Value

A new CnfAtom object.

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

mlr3pipelines documentation built on Aug. 8, 2025, 7:19 p.m.