The LCNF Formalism

The LCNF representation combines a propositional logic formula with a set of metric constraints. The key to the encoding is the simple but expressive concept of triggers -- each propositional variable may ``trigger'' a constraint; this constraint is then enforced whenever the trigger variable's truth assignment is true.

Formally, an LCNF problem is a five-tuple $\langle{\mbox{$\cal R$}, \mbox{$\cal V$}, \mbox{$\Delta$}, \mbox{$\Sigma$}, \mbox{$\cal T$}}\rangle$ in which $\cal R$ is a set of real-valued variables, $\cal V$ is a set of propositional variables, $\Delta$ is a set of linear equality and inequality constraints over variables in $\cal R$, $\Sigma$ is a propositional formula in CNF over variables in $\cal V$, and $\cal T$ is a function from $\cal V$ to $\Delta$ which establishes the constraint triggered by each propositional variable. We require that $\Delta$ contain a special null constraint which is vacuously true, and this is used as the $\cal T$-value for a variable in $\cal V$ to denote that it triggers no constraint. Moreover, for each variable v we define $\mbox{$\cal T$}(\neg v)=\verb*\vert null\vert$.

Under this definition, an assignment to an LCNF problem is a mapping, $\varphi$, from the variables in $\cal R$ to real values and from the variables in $\cal V$ to truth values. Given an LCNF problem and an assignment, the set of active constraints is $\{{c \in \mbox{$\Delta$}\vert \exists v \in \mbox{$\cal V$}\ \ \varphi(v)={\tt true} \wedge \mbox{$\cal T$}(v)=c}\}$. We say that an assignment satisfies the LCNF problem if and only if it makes at least one literal true in each clause of $\Sigma$ and satisfies the set of active constraints.

Figure 2: Portion of a tiny LCNF logistics problem (greatly simplified from compiler output). A truck with load and fuel limits makes a delivery but is too small to carry all load available (the AllLoaded constraint). Italicized variables are boolean-valued; typeface are real.

Figure 2 shows a fragment of a sample LCNF problem: a truck, which carries a maximum load of 30 and fuel level of 15, can make a Delivery by executing the Move action. We discuss later why it cannot have a GoodTrip.