• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Computational Complexity of Automated Theorem Proving

Research Project

Project/Area Number 08044158
Research Category

Grant-in-Aid for international Scientific Research

Allocation TypeSingle-year Grants
SectionJoint Research .
Research Field 計算機科学
Research InstitutionKYOTO UNIVERSITY (1997)
Kyushu University (1996)

Principal Investigator

IWAMA Kazuo  Graduate School of Engineering, Professor, 工学研究科, 教授 (50131272)

Co-Investigator(Kenkyū-buntansha) PAUL Purdom  Indiana University, CS,Professor, 計算機科学科, 教授
RUSSELL Impagliazzo  University of California San Diego, CS & E,Associate Professor, 計算機科学科, 助教授
SAKURAI Kouichi  Kyushu University, CS & CE,Associate Professor, 大学院・システム情報科学研究科, 助教授 (60264066)
TONIANN Pitassi  University of Arizona, CS,Assistant Professor, 計算機科学科, 助教授
IMPAGLIAZZO ラッセル  カリフォルニア大学(サンジエゴ校), 計算機科学科, 助教授
PITASSI Toni  アリゾナ大学, 計算機科学科, 助教授
Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 1997: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1996: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywordstheorem proving / Resolution / computational complexity / 定理の自動証明 / NP完全性 / SAT
Research Abstract

Automated theorem proving system is one of the most popular topics of AI field and has been discussed by many researchers. However, there is no perspective of making it into practical use because of the lack of fundamental analysis on it. In this research work, we discussed the intractability of Resolution, a theorem proving system of tautology. We obtained the following results :
(1) A lot of effort has been done for the problem of finding Resolution proofs and fast algorithms are developed recently. We analyzed this problem in terms of optimization, i.e., the problem of finding shortest Resolution proofs. We showed that the problem of finding a proof of length less than S+O(n^d) is NP-hard, where n is the number of variables, S is the length of the shortest proof, and d is an arbitrary constant.
(2) We discussed the relation between Resolution and Backtracking method, an algorithm for CNF Satisfiability problem (SAT). We showed that a search tree of Backtracking can be obtained from Resolution proof without increasing the size of the tree, and vice versa.
(3) We found a set of CNF formulas such that we can reduce the length of the proof by adding redundancy. Let NH be the set of formulas obtained by translating some graph problem into SAT.NH needs exponential length of Resolution proof. However, if we add small number of clauses to formulas in NH,we can prove NH in polynomial number of steps. In some occasions, we solve hard combinatorial problems translating into SAT.In this case, it seems reasonable to translate the original problem into short formulas. However, our result shows that there are some occasions in which redundancy plays an important role.

Report

(3 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • Research Products

    (32 results)

All Other

All Publications (32 results)

  • [Publications] Iwama,K.,: "A canonical from of vector machines" Information and Computation. (to appear).

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "Better approximations of non-Hamiltonian graphs" Discrete Applied Mathematics. 81. 239-261 (1998)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "Complexity of Finding Short Resolution Proofs" Proc.22nd Symposium on Mathematical Foundation of Computer Sceince(MFCS'97). LNCS1295. 309-318 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "Three-dimensional mashes are less powerful than two-dimesional ones in oblivious routing" Proc.Fifth Europian Symposium on Algorithms(ESA'97). LNCS1284. 284-295 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "Local search algorithms for partial MAXSAT" Proc.AAAI'97. 263-268 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.,: "Random benchmark circuits with controlled attributes" Proc.European Design & Test Conference and Exhibition(ED&TC'97). 90-97 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "A faster parallel algorithm for k-connectivity" Information Processing Letters. 61. 265-269 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama,K.: "Oblivious routing algorithms on the mesh of buses" Proc.11th International Parallel Processing Symposium. 721-727 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K.and Iwamoto, C.: "A canonical form of vector machines" Information and Computation. (to appear).

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K.and Miyano, E.: "Better approximations of non-Hamiltonian graphs" Discrete Applied Mathematics. Vol.81. 239-261 (1998)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K.: "Complexity of Finding Short Resolution Proofs" Proc.MFCS'97. LNCS 1295. 309-318 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K.and Miyano, E.: "Three-dimensional mashes are less powerful than two-dimesional ones in oblivious routing" Proc.ESA'97. LNCS 1284. 284-295 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Cha, B., Iwama, K., Kambayashi, Y.and Miyazaki, S.: "Local search algorithms for partial MAXSAT" Proc.AAAI'97. 263-268 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K., Hino, K., Kurokawa, H.and Sawada, S.: "Random benchmark circuits with controlled attributes" Proc.ED&TC'97. 90-97 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Iwama, K.: "A canonical form of vector machines" Information and Computation. (to appear).

    • Related Report
      1997 Annual Research Report
  • [Publications] Iwama, K.: "Better approximations of non-Hamiltonian graphs" Discrete Applied Mathematics. 81. 239-261 (1998)

    • Related Report
      1997 Annual Research Report
  • [Publications] Iwama, K.: "Complexity of Finding Short Resolution Proofs" Proc.22nd Symposium on Mathematical Foundation of Computer Sceince(MFCS'97). LNCS1295. 309-318 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Iwama, K.: "Three-dimensional mashes are less powerful than two-dimesional ones in oblivious routing" Proc.Fifth Europian Symposium on Algorithms(ESA'97). LNCS1284. 284-295 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Iwama, K.: "Local search algorithms for partial MAXSAT" Proc.AAAI' 97. 263-268 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Iwama, K.: "Random benchmark circuits with controlled attributes" Proc.European Design & Test Conference and Exhibition(ED&TC' 97). 90-97 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 岩間,一雄: "α-connectivity : A gradually non-parallel graph problem" Journal of Algorithms. 20・3. 526-544 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Routing problems on the mesh of buses" Journal of Algorithms. 20・3. 613-631 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "A faster parallel algorithm for κ-connecitivity" Proc.KOREA-JAPAN Joint Workshop on Algorithms and Computation. 8-13 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 櫻井,幸一: "A hidden cryptographic assumption in no-transferable identification schemes" Advances in Cryptology-Asiacrypt'96,Lecture Notes in Computer Science. (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Database queries as combinatorial optimization problems" Proc.Int.Sympo.on Cooperative Database Systems for Advanced Applications. 448-454 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Random benchmark circuits with controlled attributes" European Design & Test Conference,ED & TC-97. (発表予定). (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Adding new clauses for faster local search" Proc.13th National Conference on Artificial Intelligence. 304-310 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Oblivious Routing Algorithms on the Mesh of Buses" Proc.International Parallel Processing Symposium (IPPS'97). (発表予定). (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩間,一雄: "Local search algorithms for partial MAXSAT" Proc.AAAI'97. (発表予定). (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] Pitassi,Toniann: "Simplified and improved resolution lower bounds" Proc.IEEE Symposium on Foundation of Computer Science. 274-282 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Impagliazzo,Russell: "Using the Groebner basis algorithm to find proofs of unsatisfiability" Proc.ACM Symposium on Theory of Computing. 174-183 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Purdom,Paul: "Backtracking and Probing" SIAM J.Comput.(発表予定). (1997)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi