• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Learning for SAT and MINSAT, and algorithms for quantified SAT and MINSAT.
【24h】

Learning for SAT and MINSAT, and algorithms for quantified SAT and MINSAT.

机译：学习SAT和MINSAT，以及量化SAT和MINSAT的算法。

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

摘要

In many logic programming applications, one must prove a large number of theorems of axioms specified by a given propositional logic formula in conjunctive normal form (CNF). When each such theorem is a CNF clause, as is typically the case, then each case becomes a SAT (satisfiability problem) instance that is derived from the given CNF formula by fixing some variables. Thus, the instances are closely related, and one should be able to learn how to solve them quickly. A related situation exists for the logic minimization problem MINSAT, where costs are associated with the assignment of True/False values, and where minimum-cost solutions have to be obtained. A problem instance is derived from a given CNF formula by fixing some of the variables. We have developed a solution algorithm for SAT and MINSAT and have implemented it in existing logic programming software called the Leibniz System. It is based on decomposition of the original instance and on backtracking search. A learning process, which is applied to classes of SAT and MINSAT, has been integrated into the compiler of the Leibniz System. We tested the solution algorithm and the learning process on a number of SAT and MINSAT cases. Learning leads to dramatic speedups of the measured worst-case run times. In many cases, we also obtained very low solution-time bounds after learning.; SAT and MINSAT are at the first level of the polynomial hierarchy. Some expert systems demand the solution of problems at higher levels of that hierarchy. We define three problems Q-ALL SAT, Q-MIN UNSAT, and Q-MAX MINSAT at the second level of the polynomial hierarchy that are of much interest, for example, for diagnostic systems. For each problem, we describe a solution algorithm. As in the SAT and MINSAT case, real applications give rise to classes of Q-ALL SAT, Q-MIN UNSAT, and Q-MAX MINSAT. Using a compiler, we describe a solution algorithm that is effective for all instances in specific classes.
机译：在许多逻辑编程应用中，必须证明由合取范式（CNF）的给定命题逻辑公式指定的大量公理定理。当每个这样的定理是CNF子句时（通常是这种情况），则每种情况都变成一个SAT（可满足性问题）实例，该实例通过固定一些变量从给定的CNF公式中得出。因此，这些实例是紧密相关的，并且人们应该能够学习如何快速解决它们。逻辑最小化问题MINSAT存在一种相关情况，其中成本与 True / False 值的分配相关，并且必须获得最低成本的解决方案。通过修复某些变量，可以从给定的CNF公式得出问题实例。我们已经为SAT和MINSAT开发了一种求解算法，并已在称为Leibniz System的现有逻辑编程软件中实现了该算法。它基于原始实例的分解和回溯搜索。应用于SAT和MINSAT类的学习过程已集成到Leibniz系统的编译器中。我们在许多SAT和MINSAT案例中测试了求解算法和学习过程。学习可以极大地加快所测得的最坏情况下的运行时间。在许多情况下，我们在学习后也获得了非常低的求解时间范围。 SAT和MINSAT在多项式层次结构的第一级。一些专家系统要求在该层次结构的更高级别上解决问题。我们在多项式层次结构的第二层定义了三个非常重要的问题，例如诊断系统，它们分别是Q-ALL SAT，Q-MIN UNSAT和Q-MAX MINSAT。对于每个问题，我们都描述一种解决方案算法。像在SAT和MINSAT情况下一样，实际应用产生了Q-ALL SAT，Q-MIN UNSAT和Q-MAX MINSAT类别。我们使用编译器描述一种解决方案算法，该算法对特定类中的所有实例均有效。

著录项

  • 作者

    Remshagen, Anja.;

  • 作者单位

    The University of Texas at Dallas.;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号