CnfClause: Clauses in CNF Formulas

In mlr3pipelines: Preprocessing Operators and Pipelines for 'mlr3'

Clauses in CNF Formulas

Description

A CnfClause is a disjunction of CnfAtom objects. It represents a statement that is true if at least one of the atoms is true. These are for example of the form

  X %among% c("a", "b", "c") | Y %among% c("d", "e", "f") | ...

CnfClause objects can be constructed explicitly, using the CnfClause() constructor, or implicitly, by using the | operator on CnfAtoms or other CnfClause objects.

CnfClause objects which are not tautologies or contradictions are named lists; the value ranges of each symbol can be accessed using [[, and these clauses can be subset using [ to get clauses containing only the indicated symbols. However, to get a list of CnfAtom objects, use as.list(). Note that the simplified form of a clause containing a contradiction is the empty list.

Upon construction, the CnfClause is simplified by (1) removing contradictions, (2) unifying atoms that refer to the same symbol, and (3) evaluating to TRUE if any atom is TRUE. Note that the order of atoms in a clause is not preserved.

Using CnfClause() on lists that contain other CnfClause objects will create a clause that is the disjunction of all atoms in all clauses.

If a CnfClause contains no atoms, or only FALSE atoms, it evaluates to FALSE. If it contains at least one atom that is always true, the clause evaluates to TRUE. These values can be converted to, and from, logical(1) values using as.logical() and as.CnfClause().

CnfClause objects can be negated using the ! operator, and combined using the & operator. Both of these operations return a CnfFormula, even if the result could in principle be represented as a single CnfClause.

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

Usage

CnfClause(atoms)

as.CnfClause(x)

Arguments

atoms	(list of (CnfAtom | CnfClause)) A list of CnfAtom or other CnfClause objects. The clause represents the disjunction of these atoms.
x	(any) The object to be coerced to a CnfClause by as.CnfClause. Only logical(1), CnfAtom, and CnfClause itself are currently supported.

Details

We are undecided whether it is a better idea to have as.list() return a named list or an unnamed one. Calling as.list() on a CnfClause with a tautology returns a tautology-atom, which does not have a name. We currently return a named list for other clauses, as this makes subsetting by name commute with as.list(). However, this behaviour may change in the future.

Value

A new CnfClause object.

See Also

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

Examples

u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
Y = CnfSymbol(u, "Y", c("d", "e", "f"))

CnfClause(list(X %among% c("a", "b"), Y %among% c("d", "e")))
cls = X %among% c("a", "b") | Y %among% c("d", "e")
cls

as.list(cls)

as.CnfClause(X %among% c("a", "b"))

# The same symbols are unified
X %among% "a" | Y %among% "d" | X %among% "b"

# tautology evaluates to TRUE
X %among% "a" | X %among% "b" | X %among% "c"

# contradictions are removed
X %among% "a" | Y %among% character(0)

# create CnfFormula:
!(X %among% "a" | Y %among% "d")

# also a CnfFormula, even if it contains a single clause:
!CnfClause(list(X %among% "a"))
(X %among% c("a", "c") | Y %among% "d") &
  (X %among% c("a", "b") | Y %among% "d")

mlr3pipelines documentation built on Sept. 30, 2024, 9:37 a.m.