Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (revision 6eed619c3a4823cae4e1aa0fece8eb1c0cbcc591)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
@@ -406,4 +406,7 @@
The combination of the assertion satisfaction elements of the problem with the conversion-cost model of \CFA{} makes this logic-solver approach difficult to apply in \CFACC{}, however.
Expressing assertion resolution as a satisfiability problem ignores the cost optimization aspect, which is necessary to decide among what are often many possible satisfying assignments of declarations to assertions.
+\cbstartx
+(MaxSAT solvers \cite{Morgado13}, which allow weights on solutions to satisfiability problems, may be a productive avenue for future investigation.)
+\cbendx
On the other hand, the deeply-recursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming.
To maintain a well-defined programming language, any optimization algorithm used must provide an exact (rather than approximate) solution; this constraint also rules out a whole class of approximately-optimal generalized solvers.