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.