Changeset 71a12390
 Timestamp:
 Apr 24, 2019, 11:50:11 AM (3 years ago)
 Branches:
 aaronthesis, armeh, cleanupdtors, jacob/cs343translation, jenkinssandbox, master, newast, newastuniqueexpr
 Children:
 ec92b48
 Parents:
 6eed619
 Location:
 doc
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

doc/bibliography/pl.bib
r6eed619 r71a12390 4065 4065 number = 1, 4066 4066 pages = {115}, 4067 } 4068 4069 @article{Morgado13, 4070 keywords = {expression resolution}, 4071 contributer = {a3moss@uwaterloo.ca}, 4072 title={Iterative and coreguided {MaxSAT} solving: A survey and assessment}, 4073 author={Morgado, Antonio and Heras, Federico and Liffiton, Mark and Planes, Jordi and MarquesSilva, Joao}, 4074 journal={Constraints}, 4075 volume={18}, 4076 number={4}, 4077 pages={478534}, 4078 year={2013}, 4079 publisher={Springer} 4067 4080 } 4068 4081 
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.