Reasoning about Knowledge by SAT Solving

Traditional knowledge reasonings rely on the general theorem provers and may suffer the state explosion problem and can only deal with toy examples. A more concrete model of knowledge called knowledge structure has been introduced by us (Su et al., 2004), which presents a BDD-based approach for computing knowledge and shows great improvement. But this BDD-based approach still has a substantial state explosion problem. In this paper, based on the knowledge structure, we illustrate an alternative and effective way by SAT solving for the knowledge reasoning in a group of agents, since SAT can be much more powerful in dealing with the state explosion problem than BDDs