Development of Practical Techniques for All Soltuion Enumeration of Large-scale Constraint Satisfaction Problems

2021 Fiscal Year Final Research Report

• Project/Area Number: 17K17725
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Intelligent informatics; Theory of informatics
• Research Institution: The University of Electro-Communications
• Principal Investigator: Toda Takahisa 電気通信大学, 大学院情報理工学研究科, 准教授 (50451159)
• Project Period (FY): 2017-04-01 – 2022-03-31
• Keywords: 制約充足問題 / SATソルバー / モデル検査 / 反例解析 / セキュリティ / プライバシ

Outline of Final Research Achievements

In this research, we developed an efficient method for computationally hard problems that intrinsically require us to enumerate all solutions of constraint satisfaction problems (CSPs). As a major achievement, we developed a computer-aided method to help us to locate faults in the designs of hardware and software. Model checking is a widely applied method for the verification and debugging of information systems. A counterexample is detected from an erroneous system as a proof of error by executing model checking, however, there is a big gap between computing counterexamples and locating faults. We thus proposed a method for providing information regarding error in a more understandable form than counterexamples by abstracting many counterexamples, which is expected to aid us in moving a trace of failure (i.e., a counterexample) to an understanding of the essence of the failure.
Beside the model checking application, we tackled security/privacy-related researches.

Free Research Field

知能情報学

Academic Significance and Societal Importance of the Research Achievements

情報システムは現代社会の基盤技術であり、特にセキュリティ、プライバシ、人命などが関わる場面では情報システムの高い品質が求められる。しかし、そのような品質の保証や解析に関わる技術は一般に計算コストが高く、本来的に完全な自動化は見込めないことが多い。本研究の主要な成果として、検証やテスト目的で広く使われている技術（モデル検査）に対してより高度な解析機能を追加した。これにより人手で行われる解析作業を一部自動化することが可能になる。モデル検査以外にもセキュリティ・プライバシーに関わる研究成果も得られ、制約充足に関する最新技術を活用した応用研究の新しい展開につながった。