Chop-SAT: A New Method for Knowledge-Based Agent Decision Making

Logical agents base their action selection decisions on inferences made over a logical knowledge base. Given a propositional logic knowledge base expressed in Conjunctive Normal Form (CNF), the knowledge can be converted into a geometrical format, and subsequent analysis takes place as geometrical operations on the feasible region in that representation. We present two novel methods based on this approach in order to: (1) find SAT solutions for the knowledge base (i.e., a truth assignment to each logical variable which makes the CNF sentence true), and (2) find a reasonable approximation to the atom probabilities given the current set of information. This allows agents to determine the semantics (truth) of the world as well as to estimate the probability of truth.