 Timestamp:
 Apr 24, 2019, 11:50:11 AM (3 years ago)
 Branches:
 aaronthesis, armeh, cleanupdtors, enum, forallpointerdecay, jacob/cs343translation, jenkinssandbox, master, newast, newastuniqueexpr
 Children:
 ec92b48
 Parents:
 6eed619
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

doc/theses/aaron_moss_PhD/phd/resolutionheuristics.tex
r6eed619 r71a12390 406 406 The combination of the assertion satisfaction elements of the problem with the conversioncost model of \CFA{} makes this logicsolver approach difficult to apply in \CFACC{}, however. 407 407 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. 408 \cbstartx 409 (MaxSAT solvers \cite{Morgado13}, which allow weights on solutions to satisfiability problems, may be a productive avenue for future investigation.) 410 \cbendx 408 411 On the other hand, the deeplyrecursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming. 409 412 To maintain a welldefined programming language, any optimization algorithm used must provide an exact (rather than approximate) solution; this constraint also rules out a whole class of approximatelyoptimal generalized solvers.
Note: See TracChangeset
for help on using the changeset viewer.