Our first step in constructing the LPSAT engine was to choose solvers to use as the foundation for its metric and propositional solving portions. The choice was motivated by the following criteria:

- 1.
- It must be easy to modify the propositional solver in order to
support triggers and handle reports of inconsistency from the constraint
reasoner.
- 2.
- The metric solver must support incremental modifications to
the constraint set.
- 3.
- Because a Simplex solve is more expensive than setting a single propositional variable's value, the propositional solver should minimize modifications to the constraint set.

These principles led us to implement the LPSAT engine by modifying
the RELSAT satisfiability engine [Bayardo and Schrag1997] and combining
it with the CASSOWARY constraint
solver [Borning *et al.*1997,Badros and
Borning1998] using the method
described in [Nelson and Oppen1979]. RELSAT makes an excellent start
for processing LCNF for three reasons. First, it performs a
systematic, depth-first search through the space of partial truth
assignments; this minimizes changes to the set of active metric
constraints. Second, the code is exceptionally well-structured.
Third, RELSAT incorporates powerful learning and backjumping
optimizations. CASSOWARY is an appropriate Simplex solver for
handling LCNF because it was designed to support and quickly respond
to small changes in its constraint set.

In order to build LPSAT, we modified RELSAT to include trigger
variables and constraints. This required four changes. First, the
solver must trigger constraints as the truth assignment changes.
Second, the solver must now check for a solvable constraint set to
ensure that a truth assignment is satisfying. Third, the solver must
report in its solution not only a truth assignment to the boolean
variables, but an assignment of real values to the constraint
variables^{4}. Finally, since even a
purely positive trigger variable may (if set to `true`) trigger an
inconsistent constraint, pure literal elimination cannot act on
*positive* trigger variables^{5}. Figure 3 displays pseudocode for the
resulting algorithm.