• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Algorithms for satisfiability problems in linear integer arithmetic logic.
【24h】

Algorithms for satisfiability problems in linear integer arithmetic logic.

机译：线性整数算术逻辑中的可满足性问题的算法。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Recent advances in solving propositional satisfiability problems (SAT) have extended their applications to several domains including design verification and synthesis, program analysis, scheduling and temporal reasoning. Current methods for solving these problems mostly suffer from poor scalability especially when more expressive atoms from different theories are involved. In such cases methods such as abstraction or bit-vector conversion are adopted to translate the problem into a Boolean formula to be solved by a SAT solver. This conversion considerably affects the efficiency of the overall process. Nonetheless, the capability of SAT algorithms to solve large problems with tens of thousand of constraints over thousands of Boolean variables has brought them into the spotlight to be used for solving problems involving combination of different theories including linear and non-linear arithmetic.;In this work, we present new scalable SAT-based algorithms for solving first-order linear integer arithmetic logic. We address problems involving arithmetic operations over Boolean variables (the so-called Pseudo-Boolean problems) as well as first-order formulas involving arithmetic operations over integer variables (the so-called Satisfiability Modulo Theories problems). In the latter case, we incorporate theory solvers for the conjunctions of "cheap" linear integer constraints, i.e. equalities and two-variable inequalities, within the SAT solver. These theory solvers are tightly but gradually integrated into the SAT solver and the problem is modeled such that the SAT solver is maximally utilized in order to leverage its power and efficiency. To curb the cost of processing "hard" constraints, i.e. general linear integer constraints, a subset of them are only added to the problem when/if the satisfiability of the rest of the problem is established. We also develop a set of algorithms to optimize the overall process taking into account special structures of the problems arising from design verification applications.;These methods, implemented in our two solvers, Pueblo and Ario, have been applied to several problems in software verification, electronic design automation (EDA) and scheduling. In this work, we describe some of these applications and present advantages of our method in a few of them, mainly in hardware and software verification and temporal reasoning.
机译：解决命题可满足性问题（SAT）的最新进展已将其应用扩展到多个领域，包括设计验证和综合，程序分析，调度和时间推理。解决这些问题的当前方法主要受可扩展性差的困扰，特别是当涉及来自不同理论的更具表现力的原子时。在这种情况下，采用诸如抽象或位向量转换之类的方法将问题转换为布尔公式，以便由SAT解算器解决。这种转换极大地影响了整个过程的效率。尽管如此，SAT算法能够解决数千个布尔变量上的成千上万个约束的大问题，使它们成为解决包括线性和非线性算术在内的不同理论组合问题的焦点。在工作中，我们提出了基于可扩展SAT的新算法来求解一阶线性整数算术逻辑。我们将解决涉及对布尔变量进行算术运算的问题（即所谓的伪布尔问题），以及涉及对整数变量进行算术运算的一阶公式（即可满足性模理论问题）。在后一种情况下，我们在SAT求解器中并入了用于“便宜”线性整数约束（即等式和二元不等式）的合点的理论求解器。这些理论求解器紧密但逐渐地集成到SAT求解器中，并对问题进行了建模，以便最大程度地利用SAT求解器以利用其功能和效率。为了抑制处理“硬”约束（即一般的线性整数约束）的成本，仅当/如果确定其余问题的可满足性时，才将其子集添加到问题中。我们还开发了一套算法来优化整个流程，同时考虑到设计验证应用程序所产生问题的特殊结构。这些方法在我们的两个求解器Pueblo和Ario中实现，已应用于软件验证中的若干问题，电子设计自动化（EDA）和计划。在这项工作中，我们描述了其中一些应用程序，并在其中一些应用程序中展示了我们方法的优势，主要是在硬件和软件验证以及时间推理方面。

著录项

  • 作者

    Sheini, Hossein Mohsen.;

  • 作者单位

    University of Michigan.;

  • 授予单位 University of Michigan.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 2006
  • 页码 198 p.
  • 总页数 198
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号