Converting logical formulae into geometrical shapes in order to solve problems in symbolic logic

Thomas C. Henderson, Amelia Lessen, Ishaan Rajan, Tessa Nishida, Kutay Eken, Xiuyi Fan, David Sacharny, Amar Mitiche, Thatcher Geary, GEO-SAT: A new approach for knowledge-based agent decision making, Robotics and Autonomous Systems, Volume 203, 2026, 10.1016/j.robot.2026.105522.

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; we will refer to a logical well-formed formula in CNF as a sentence), the knowledge can be converted into a geometrical format, and subsequent analysis takes place as geometrical operations on the feasible region in that representation. Two geometric representations are presented: the n-dimensional hypercube in Euclidean geometry and the n-dimensional Poincaré disk in non-Euclidean geometry. Based on these representations, two novel methods are proposed to: (1) find SAT solutions for the knowledge base (i.e., a truth assignment to each logical variable which makes the 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. The geometric method provides an efficient heuristic approach to solving SAT for CNF knowledge bases, and provides polynomial-time solutions of probabilistic SAT (PSAT) for independent variables, and good PSAT estimates for non-independent logical variables. The polynomial time result for PSAT is due to the fact that the feasible region for the logical sentence is found using convex linear programming, and any point in the feasible region provides a set of valid atom probabilities. From these, if the variables are independent, any complete conjunction is defined as the product of literal probabilities. There is still no reduction of SAT to a geometric problem with a polynomial time solution; this approach to solving SAT and PSAT is called GEO-SAT.

Comments are closed.

Post Navigation