Changeset 71a12390 for doc/theses/aaron_moss_PhD

Timestamp:

Apr 24, 2019, 11:50:11 AM (5 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

ec92b48

Parents:

6eed619

Message:

thesis: address comment about MaxSAT

File:

• doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (modified) (1 diff)

doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

@@ -406 +406 @@
 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.