Index: doc/bibliography/pl.bib
===================================================================
--- doc/bibliography/pl.bib	(revision 6eed619c3a4823cae4e1aa0fece8eb1c0cbcc591)
+++ doc/bibliography/pl.bib	(revision 71a12390eb03a6fdd2beefb60f5a0838f37b2ea8)
@@ -4065,4 +4065,17 @@
     number	= 1,
     pages	= {1-15},
+}
+
+@article{Morgado13,
+  keywords = {expression resolution},
+  contributer = {a3moss@uwaterloo.ca},
+  title={Iterative and core-guided {MaxSAT} solving: A survey and assessment},
+  author={Morgado, Antonio and Heras, Federico and Liffiton, Mark and Planes, Jordi and Marques-Silva, Joao},
+  journal={Constraints},
+  volume={18},
+  number={4},
+  pages={478--534},
+  year={2013},
+  publisher={Springer}
 }
 
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.