Changeset 71a12390


Ignore:
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

Location:
doc
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • doc/bibliography/pl.bib

    r6eed619 r71a12390  
    40654065    number      = 1,
    40664066    pages       = {1-15},
     4067}
     4068
     4069@article{Morgado13,
     4070  keywords = {expression resolution},
     4071  contributer = {a3moss@uwaterloo.ca},
     4072  title={Iterative and core-guided {MaxSAT} solving: A survey and assessment},
     4073  author={Morgado, Antonio and Heras, Federico and Liffiton, Mark and Planes, Jordi and Marques-Silva, Joao},
     4074  journal={Constraints},
     4075  volume={18},
     4076  number={4},
     4077  pages={478--534},
     4078  year={2013},
     4079  publisher={Springer}
    40674080}
    40684081
  • doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

    r6eed619 r71a12390  
    406406The 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.
    407407Expressing 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
    408411On the other hand, the deeply-recursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming.
    409412To 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.
Note: See TracChangeset for help on using the changeset viewer.