Formally, an LCNF *problem* is a five-tuple
in which
is a set of real-valued variables,
is a set of propositional
variables,
is a set of linear equality and inequality constraints
over variables in ,
is a propositional formula in CNF over
variables in ,
and
is a function from
to
which
establishes the constraint triggered by each propositional variable.
We require that
contain a special `null`

constraint which is
vacuously true, and this is used as the -value for a variable in
to denote that it triggers no constraint. Moreover, for each
variable *v* we define
.

Under this definition, an assignment to an LCNF problem is a
mapping, ,
from the variables in
to real values and from
the variables in
to truth values. Given an LCNF problem and an
assignment, the *set of active constraints* is
.
We
say that an assignment *satisfies* the LCNF problem if and only
if it makes at least one literal true in each clause of
and
satisfies the set of active constraints.

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