运筹学是从20世纪40年代发展起来的重要学科，最优化（又称数学规划）是运筹学的重要问题之一，它关注在一定变量的约束条件下寻找给定目标函数的最大值或最小值。绝大多数学者研究优化问题时都默认其约束公式间关系是逻辑“与”。但是，随着各领域应用需求的增多，优化问题逐渐含有诸如布尔代数、分段函数、max-min不等式、离散映射、集合划分等特征的约束，这些约束无法仅用逻辑“与”而必须要引入逻辑“或”连接的公式才能够描述。本文将传统约束优化问题进行拓展，把同时含有逻辑“与”和“或”约束的优化问题称为广义约束优化问题。目前对一般性的广义约束优化算法的研究还非常少，同时由于该问题可行域的非凸性以及约束条件的复杂性，对设计高效的求解算法带来了困难与挑战。　　优化模理论(OMT)是理论计算机科学的一门新兴分支学科，它是可满足性模理论(SMT)的拓展。OMT问题寻找满足具有背景理论（如线性算术、数组、位向量等）逻辑公式的解并使得某个代价函数达到最大或最小。在线性算术背景理论下的OMT问题是一类特殊的广义约束优化问题，它不仅需要在含有逻辑“与”和“或”连接的线性算术公式约束下最优化某个线性函数，还必须在SMT的框架下进行求解以适应其它组合背景理论的逻辑可满足性。　　本文同时从运筹学和OMT两方面对广义约束优化问题的算法理论与典型应用开展研究。首先从SMT的角度，提出线性算术OMT改进算法;随后，研究一般线性情形的广义约束优化问题，提出一种全新并具有通用性的广义约束优化算法，以适应更广泛的应用场景;最后将全新的广义约束优化算法应用到实时系统领域，研究单调速率优化设计问题及求解算法。本文的主要贡献和创新点如下:　　1.提出并实现一种线性算术OMT改进算法OPT-LA　　现有OMT求解器都是通过这两步的反复迭代搜索最优解:(1)寻找可能是全局最优的“候选解”;(2)用SMT求解器验证候选解的全局最优性。但是，这些计算出的候选解仍然有大部分在可行域中存在使目标函数优化的方向，它们不可能是最优解，因此没有必要开销大量时间调用SMT求解器进行全局最优性验证。本文提出的OPT-LA能有效避免这个缺点。OPT-LA每次寻找候选解时，通过在可行域中构造序列凸可行域并朝着对应线性规划问题最优解的方向进行搜索，使收敛得到的候选解不存在使函数优化的方向（即局部最优解），从而减少候选解总数，达到降低SMT求解器调用次数及减少总运行时间的目的。实验结果表明，OPT-LA能平均减少60％的候选解数量，算法最大加速比达到200倍。　　2.提出并实现一种全新且具有通用性的广义约束优化算法OPT-DC　　现有算法都不可避免地使用剪枝搜索在非凸可行域中寻找最优解，但是它们存在两类缺点:(1)记录大量剪枝节点信息，随着搜索迭代次数的增加使约束公式数量爆炸式增长，严重影响搜索效率;(2)节点信息依赖其父节点的计算结果，具有不确定性，制约了剪枝策略的设计和扩展。本文提出的OPT-DC能克服这两类缺点。OPT-DC的搜索过程在一棵各节点为线性规划问题的搜索树上以深度优先的方式进行，并且节点的构造是有序的，所以其搜索方式无需记录剪枝节点信息，同时保证了每个节点信息的确定性以方便剪枝策略的设计和扩展。然后在基于OPT-DC的搜索方式上设计了3个可独立使用的策略来提升剪枝搜索的效率。OPT-DC具有全局最优收敛性。实验结果表明，OPT-DC同时在计算高效性和结果准确性上优于其它算法，并且问题规模越大优势越明显。　　3.提出并实现一种实时系统单调速率优化设计算法LPS　　现有的单调速率优化设计算法存在2个问题:(1)将问题转换为传统非线性约束优化问题求解，但该问题是非凸的，目前没有相应的非线性优化算法能得到全局最优解;(2)将问题转换为整数规划问题求解，但搜索空间呈指数增长且节点信息具有不确定性。本文借助OPT-DC算法，提出一种新的单调速率优化设计算法LPS。LPS在基于单调速率调度的特点上对OPT-DC进行了改造:用单调速率可调度性充要条件中的各任务测试时间点来表示各节点的线性规划问题，减少冗余的不等式生成计算;根据各线性规划子问题约束不等式的系数都是非负的，简化OPT-DC中利用区间分析删除不等式的过程;利用CPU利用率的上下界，使OPT-DC中的非参数估计方法误差更小，进一步提升目标函数最大值下界。实验结果表明LPS能为最多100个任务设计运行时间，平均加速比达4倍。