| 2014 | KR | Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas. | Yuping Shen, Xishun Zhao |
| 2012 | SAT | On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets. | Oliver Kullmann, Xishun Zhao |
| 2011 | SAT | Transformations into Normal Forms for Quantified Circuits. | Hans Kleine Bning, Xishun Zhao, Uwe Bubeck |
| 2011 | SAT | On Variables with Few Occurrences in Conjunctive Normal Forms. | Oliver Kullmann, Xishun Zhao |
| 2009 | SAT | Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits. | Hans Kleine Bning, Xishun Zhao, Uwe Bubeck |
| 2006 | SAT | Minimal False Quantified Boolean Formulas. | Hans Kleine Bning, Xishun Zhao |
| 2005 | SAT | Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas. | Uwe Bubeck, Hans Kleine Bning, Xishun Zhao |
| 2005 | SAT | Model-Equivalent Reductions. | Xishun Zhao, Hans Kleine Bning |
| 2004 | AAAI | On Odd and Even Cycles in Normal Logic Programs. | Fangzhen Lin, Xishun Zhao |
| 2004 | SAT | Equivalence Models for Quantified Boolean Formulas. | Hans Kleine Bning, Xishun Zhao |
| 2004 | SAT | Equivalence Models for Quantified Boolean Formulas. | Hans Kleine Bning, Xishun Zhao |
| 2003 | SAT | On Boolean Models for Quantified Boolean Horn Formulas. | Hans Kleine Bning, K. Subramani, Xishun Zhao |
| 2003 | SAT | Read-Once Unit Resolution. | Hans Kleine Bning, Xishun Zhao |