Next: The LPSAT Solver Up: The LPSAT Engine & Previous: Introduction

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

Next: The LPSAT Solver Up: The LPSAT Engine & Previous: Introduction

2000-02-24