Optimization of polynomial constraint solving based on fusion of approximation and algebraix methods

2014 Fiscal Year Final Research Report

• Project/Area Number: 23300005
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: MIZUHITO Ogawa 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
• Co-Investigator(Kenkyū-buntansha): SEKI Hiroyuki 名古屋大学, 情報科学研究科, 教授 (80196948) ; HIROKAWA Nao 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
• Research Collaborator: VU Xuan Tung ; TO Van Khanh
• Project Period (FY): 2011-04-01 – 2015-03-31
• Keywords: ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理

Outline of Final Research Achievements

This research extends the interval constraint propagation to the raSAT loop, which is implemented as an SMT solver raSAT. A polynomial constraint solving concludes either SAT (satisfiable) or UNSAT (unsatisfiable). raSAT is designed to intend the former, which is often used for error detection, where the latter is used for loop invariant generation. In practice, when tackling a larger problem with several hundred variables, UNSAT is detected only with the discovery of a small UNSAT core, whereas SAT is detected by finding an instance that satisfies all constraints, and often becomes a harder problem. In experiments, we newly found that several unsolved problems in SMTlib benchmark are SAT.

Free Research Field

理論計算機科学、形式手法