Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91)
+++ 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.