Forrest Bao

AAAI Conference 2015 Conference Paper

Accelerating SAT Solving by Common Subclause Elimination

• Yaowei Yan
• Chris Gutierrez
• Jeriah Jn-Charles
• Forrest Bao
• Yuanlin Zhang

Boolean SATisfiability (SAT) is an important problem in AI. SAT solvers have been effectively used in important industrial applications including automated planning and verification. In this paper, we present novel algorithms for fast SAT solving by employing two common subclause elimination (CSE) approaches. Our motivation is that modern SAT solving techniques can be more efficient on CSE-processed instances. Empirical study shows that CSE can significantly speed up SAT solving.

AAAI Conference 2012 Conference Paper

Combining Probabilistic Planning and Logic Programming on Mobile Robots

• Shiqi Zhang
• Forrest Bao
• Mohan Sridharan

AAAI Conference 2012 Conference Paper

Temporally Expressive Planning Based on Answer Set Programming with Constraints

• Forrest Bao
• Yuanlin Zhang

Recently, a new language AC(C) was proposed to integrate answer set programming (ASP) and constraint logic programming (CLP). In this paper, we show that temporally expressive planning problems in PDDL2. 1 can be translated into AC(C) and solved using AC(C) solvers. Compared with existing approaches, the new approach puts less restrictions on the planning problems and is easy to extend with new features like PDDL axioms. It can also leverage the inference engine for AC(C) which has the potential to exploit the best reasoning mechanisms developed in the ASP, SAT and CP communities. More details, including the proof to the correctness of the translation, are provided online at https: //sites. google. com/site/pddl2acc/