Research and Development on Constraint Answer Set Programming Using SAT Encoding

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00099
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Kobe University
• Principal Investigator: BANBARA Mutsunori 神戸大学, 情報基盤センター, 准教授 (80290774)
• Co-Investigator(Kenkyū-buntansha): 田村 直之 神戸大学, 情報基盤センター, 教授 (60207248) ; 宋 剛秀 神戸大学, 情報基盤センター, 助教 (00625121)
• Co-Investigator(Renkei-kenkyūsha): INOUE Katsumi 国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
• Project Period (FY): 2015-04-01 – 2018-03-31
• Keywords: 解集合プログラミング / 制約プログラミング / SAT技術

Outline of Final Research Achievements

We focused research and development on Constraint Answer Set Programming (CASP), an integration of Answer Set Programming (ASP) and Constraint Programming (CP). CASP allows for direct representation of Constraint Satisfaction Problems (CSPs) over finite domains of Integers. We have developed two CASP solvers. One is based on a translation-based approach where a CSP is fully translated into ASP and then solved by an ASP solver. Another is based on a lazy approach where an ASP solver is augmented with dedicated propagators for CSPs. We established the competitiveness of our approach by empirically contrasting our solvers and other different CASP/CP solvers.

Free Research Field

情報学・計算基盤・ソフトウェア