We use cookies to improve your experience with our site.

一种求解线性算数约束优化问题的高效方法

An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints

  • 摘要: 可满足性模理论在最近十年已被广泛地研究,最近研究人员将该问题拓展为在线性算数约束下的优化问题。目前有两个国际公认最好的优化求解器:Symba和OPT-MathSAT。这两个工具的主要算法由两步的循环组成:(1)关键搜寻,用于寻找可能是最优点的可行点;(2)全局检查,用于验证寻找出的可行点是不是最优点。本文提出一种新的求解线性算数约束下的优化算法,其基本原理是通过构造并求解一系列的线性规划问题寻找关键可行点,并能够将Symba和OPT-MathSAT中的关键搜寻步骤算法替换掉。实验比较了我们的方法与Symba以及OPT-MathSAT在一类实时系统关键问题上的求解效率。试验结果表明我们的方法在99.6%的问题上能够超过Symba,同时在大规模问题下优于OPT-MathSAT。实验结果表明我们的方法在求解类似的优化问题上的潜力与优势。

     

    Abstract: Satisfiability Modulo Theories (SMT) have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, Symba and OPT-MathSAT are two most efficient solvers available for this problem. The key algorithms used by Symba and OPT-MathSAT consist of the loop of two procedures: 1) critical finding for detecting a critical point, which is very likely to be globally optimal, and 2) global checking for confirming the critical point is really globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the algorithms of critical finding in Symba and OPT-MathSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against Symba and OPT-MathSAT on a critical class of problems in real-time systems. Our approach outperforms Symba on 99.6% of benchmarks and is superior to OPT-MathSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem.

     

/

返回文章
返回