• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Algorithmic applications of propositional proof complexity.
【24h】

Algorithmic applications of propositional proof complexity.

机译：命题证明复杂性的算法应用。

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

摘要

This thesis explores algorithmic applications of proof complexity theory to the areas of exact and approximation algorithms for graph problems as well as propositional reasoning systems studied commonly by the artificial intelligence and formal verification communities. On the theoretical side, our focus is on the propositional proof system called resolution. On the practical side, we concentrate on propositional satisfiability algorithms (SAT solvers) which form the core of numerous real-world automated reasoning systems.; There are three major contributions in this work. (A) We study the behavior of resolution on appropriate encodings of three graphs problems, namely, independent set, vertex cover, and clique. We prove lower bounds on the sizes of resolution proofs for these problems and derive from this unconditional hardness of approximation results for resolution-based algorithms. (B) We explore two key techniques used in SAT solvers called clause learning and restarts, providing the first formal framework for their analysis. Formulating them as proof systems, we put them in perspective with respect to resolution and its refinements. (C) We present new techniques for designing structure-aware SAT solvers based on high-level problem descriptions. We present empirical studies which demonstrate that one can achieve enormous speed-up in practice by incorporating variable orders as well as symmetry information obtained directly from the underlying problem domain.
机译：本文探讨了证明复杂性理论在图问题的精确和近似算法以及人工智能和形式验证团体通常研究的命题推理系统领域中的算法应用。从理论上讲，我们的重点是命题证明系统，称为解决方案。在实践方面，我们专注于命题可满足性算法（SAT求解器），这些算法构成了众多现实世界中自动推理系统的核心。这项工作有三大贡献。 （A）我们研究三个图形问题的适当编码下的分辨率行为，即独立集，顶点覆盖和集团。我们针对这些问题证明了分辨率证明的大小的下界，并从基于分辨率的算法的近似结果的这种无条件的硬度中得出。 （B）我们探索了SAT解算器中使用的两种关键技术，称为子句学习和重新启动，为它们的分析提供了第一个正式框架。将它们表述为证明系统，我们就分辨率及其改进对它们进行了透视。 （C）我们提出了基于高级问题描述来设计结构感知SAT求解器的新技术。我们目前的经验研究表明，通过结合可变阶数和直接从潜在问题域中获得的对称信息，可以在实践中实现巨大的提速。

著录项

  • 作者

    Sabharwal, Ashish.;

  • 作者单位

    University of Washington.;

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

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号