A Study of Advanced and Effective SAT Planning and Scheduling

点击翻译按钮获取中文摘要

Propositional satisfiability (SAT) problems and its high performance solvers are used for solving various problems, such as planning and scheduling, which are encoded into SAT instances. Generally, SAT encoding approaches need to solve multiple SAT instances. In order to solve such multiple SAT instances, we have developed a distributed and cooperative SAT solver SatCube, which reuse lemmas, hypotheses and models during the search process and can solve multiple SAT instances efficiently. We have studied SAT planning to extend the application area based on ordered encoding, and proposed various speed-up techniques for SAT scheduling.