%% 
%% Copyright 2007-2020 Elsevier Ltd
%% 
%% This file is part of the 'Elsarticle Bundle'.
%% ---------------------------------------------
%% 
%% It may be distributed under the conditions of the LaTeX Project Public
%% License, either version 1.2 of this license or (at your option) any
%% later version.  The latest version of this license is in
%%    http://www.latex-project.org/lppl.txt
%% and version 1.2 or later is part of all distributions of LaTeX
%% version 1999/12/01 or later.
%% 
%% The list of all files belonging to the 'Elsarticle Bundle' is
%% given in the file `manifest.txt'.
%% 

%% Template article for Elsevier's document class `elsarticle'
%% with numbered style bibliographic references
%% SP 2008/03/01
%%
%% 
%%
%% $Id: elsarticle-template-num.tex 190 2020-11-23 11:12:32Z rishi $
%%
%%
\documentclass[preprint,12pt]{elsarticle}

%% Use the option review to obtain double line spacing
%% \documentclass[authoryear,preprint,review,12pt]{elsarticle}

%% Use the options 1p,twocolumn; 3p; 3p,twocolumn; 5p; or 5p,twocolumn
%% for a journal layout:
%% \documentclass[final,1p,times]{elsarticle}
%% \documentclass[final,1p,times,twocolumn]{elsarticle}
%% \documentclass[final,3p,times]{elsarticle}
%% \documentclass[final,3p,times,twocolumn]{elsarticle}
%% \documentclass[final,5p,times]{elsarticle}
%% \documentclass[final,5p,times,twocolumn]{elsarticle}

%% For including figures, graphicx.sty has been loaded in
%% elsarticle.cls. If you prefer to use the old commands
%% please give \usepackage{epsfig}
\usepackage{epsfig}
\usepackage{makeidx}  % allows for indexgeneration
%
\usepackage{etoolbox} % for "\patchcmd" macro
\makeatletter
\patchcmd{\ps@headings}{\rlap{\thepage}}{}{}{}
\patchcmd{\ps@headings}{\llap{\thepage}}{}{}{}
\makeatother
\pagestyle{headings} % reload the now-modified "headings" page style
%
\usepackage{algorithm2e}
\usepackage{mathtools}
\usepackage{theorem}

%% The amssymb package provides various useful mathematical symbols
\usepackage{amssymb}
%% The amsthm package provides extended theorem environments
%% \usepackage{amsthm}

%% The lineno packages adds line numbers. Start line numbering with
%% \begin{linenumbers}, end it with \end{linenumbers}. Or switch it on
%% for the whole article with \linenumbers.
%% \usepackage{lineno}

%%\journal{Nuclear Physics B}

\begin{document}
\bibliographystyle{plain}   % Can have alpha for [He85] style

\begin{frontmatter}

%% Title, authors and addresses

%% use the tnoteref command within \title for footnotes;
%% use the tnotetext command for theassociated footnote;
%% use the fnref command within \author or \address for footnotes;
%% use the fntext command for theassociated footnote;
%% use the corref command within \author for corresponding author footnotes;
%% use the cortext command for theassociated footnote;
%% use the ead command for the email address,
%% and the form \ead[url] for the home page:
%% \title{Title\tnoteref{label1}}
%% \tnotetext[label1]{}
%% \author{Name\corref{cor1}\fnref{label2}}
%% \ead{email address}
%% \ead[url]{home page}
%% \fntext[label2]{}
%% \cortext[cor1]{}
%% \affiliation{organization={},
%%             addressline={},
%%             city={},
%%             postcode={},
%%             state={},
%%             country={}}
%% \fntext[label3]{}

\title{GEO-SAT: A New Approach for Knowledge-Based Agent Decision Making}

%% use optional labels to link authors explicitly to addresses:
%% \author[label1,label2]{}
%% \affiliation[label1]{organization={},
%%             addressline={},
%%             city={},
%%             postcode={},
%%             state={},
%%             country={}}
%%
%% \affiliation[label2]{organization={},
%%             addressline={},
%%             city={},
%%             postcode={},
%%             state={},
%%             country={}}

\author{Thomas C. Henderson, Amelia Lessen, Ishaan Rajan, Tessa
  Nishida, Kutay Eken, Xiuyu Fan, David Sacharny, Amar Mitiche and
  Thatcher Geary}

%%%%%\author{Thomas C. Henderson \and Amelia Lessen \and Ishaan Rajan \and
%%%%%  Tessa Nishida \and Kutay Eken \and Xiuyi Fan \and David Sacharny
%%%%%  \and Amar Mitiche \and Thatcher Geary}

\affiliation{organization={University of Utah},%Department and Organization
            addressline={School of Computing}, 
            city={Salt Lake City},
            postcode={84112}, 
            state={UT},
            country={USA}}

\begin{abstract}
%% Text of abstract
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.  Two geometric representations are presented:
the n-dimensional hypercube in Euclidean geometry and the n-dimensional
Poincar\'{e} 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 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.  The geometric method provides an
efficient heuristic approach to solving SAT for CNF knowledge bases,
and provides polynomial-time solutions of probabilistic SAT for
independent variables, and good PSAT estimates for non-independent
logical variables.
\end{abstract}

%%Graphical abstract
%%%%%%\begin{graphicalabstract}
%\includegraphics{grabs}
%%%%%\end{graphicalabstract}

%%Research highlights
%%%%\begin{highlights}
%%%%%\item Research highlight 1
%%%%%\item Research highlight 2
%%%%\end{highlights}

\begin{keyword}
%% keywords here, in the form: keyword \sep keyword
  Knowledge representation, geometric methods, SAT, PSAT
  
%% PACS codes here, in the form: \PACS code \sep code

%% MSC codes here, in the form: \MSC code \sep code
%% or \MSC[2008] code \sep code (2000 is the default)

\end{keyword}

\end{frontmatter}

%% \linenumbers

%% main text
\section{Introduction and Background}

Given a propositional calculus knowledge base represented in
Conjunctive Normal Form (CNF), an agent can find out information about
the world by finding new sentences that are entailed by the current
knowledge.  In this way, an agent can determine proper
actions.  To do so, it may be useful to determine whether the CNF
sentence has a solution (satisfiable) or not (unsatisfiable).
This is called the SAT problem (for SATisfiability) problem. The SAT
problem is NP complete \cite{Sipser2012}.

Another
aspect of interest to the agent is the probability that a specific
atom (logical variable) is true.  For example, for the CNF $S=A\vee
B$,
there are three solutions, {(0, 1), (1, 0), (1, 1)}, which satisfy S
and, assuming equal likelihood for all solutions, the probability of A
is 2/3, and the probability of B is 2/3
Note that
this is the mean of the models (truth assignments to variables) which
satisfy the sentence.  One way to determine the atom probabilities is
to solve the {\it Probabilistic SAT} (PSAT) problem when each
conjunct, $C_{i}$, is given a probability, $p_{i}$
\cite{Georgakopoulos1988,Nilsson1986}.  That is, given
$n$ logical variables, there are 
$2^{n}$ unique truth assignments (also called models or the complete
conjunction set) to the
variables.  The set of all models is called $\Omega$, and $\omega_{i}$
is the model with binary assignments corresponding to the binary
representation of $i-1$; e.g., $\omega_{1}$ is all zero assignments -
all false.  The PSAT problem consists of determining a probability
distribution, $\pi:\Omega\rightarrow[0,1]$ such that
$\sum_{i=1}^{2^{n}}\pi(\omega_{i})=1$, and 
$\sum_{\omega_{i}\models C_{j}}\pi(\omega_{i})=p_{j}$, for all
conjunct probabilities, $p_{i}$.
The probability of an atom is then found as $Prob(A) =
\sum_{\omega_{i}\models A}\pi(\omega_{i})$.
We have also previously described how to solve the Probabilistic
Sentence Satisfiability Problem (PSSAT) \cite{Henderson2020} which in
certain cases provides a PSAT solution (i.e., given independent
variables).  The methods we are proposing differ from standard methods
in that we solve linear or nonlinear systems of equations rather than
having to consider the full joint probability distribution over the
variables (e.g., like Bayesian networks \cite{Pearl1988} or Markov
Logic Networks \cite{Domingos2009}).

The purpose of this study is to investigate {\it Chop-SAT} as an
alternative way to answer these questions about SAT and PSAT
\cite{Henderson2021,Henderson2023}.
Work on the use of cutting planes started with Gomory \cite{Gomory1958} who
sought integer solutions for linear programs.  Given the semantics of
the literals in a
disjunction, then a linear inequality can be formed summing $x_{i}$
for atoms in the clause and $(1-x_{i})$ for negated atoms in the clause
and setting this to be greater than or equal to 1.  Next, a $\{0,1\}$
solution is sought resulting in an integer linear programming
problem.  If a non-$\{0,1\}$ solution is found, Gomory proposed a way
to separate (via a {\it cutting plane}) that solution from all integer
solutions.  This method has been used in finding lower complexity ways
to provide theorems for proving the boundedness of polytopes, cutting
plane proofs for unsatisfiable sentences, pseudo-Boolean optimization,
etc. (see
\cite{Buss1996,Chvatal1973,Chvatal1985,Cook1987,Devriendt2021}).  The
{\it Chop-SAT} method was discovered independently and is based on a
different set of insights into the nature of the CNF form.

Based on the {\it Chop-SAT} approach, the contributions here provide:
\begin{enumerate}

  \item
  A method to determine whether a SAT solution exists, and

  \item
  A method to determine an approximation to the atom probabilities.
\end{enumerate}

\section{Chop-SAT}

A CNF sentence is the conjunction of a set of disjunctions where each
disjunction is a literal (i.e., either an atom or the negation of an
atom).  A CNF sentence is then represented as 
$S = C_{1} \wedge C_{2} \wedge \ldots \wedge C_{m}$,
where $C_{i} = L_{i,1} \vee L_{i,2} \vee \ldots \vee L_{i,k_{i}}$
where $L_{i,j} = a_{p}$ or $L_{i,j} = \neg a_{p}$, and $a_{p}$ is an
atom.

The satisfiability of a CNF sentence, $S$, over $n$ variables can be
converted to a geometric
problem as follows. Consider the hypercube of dimension $n$ centered
at $[\frac{1}{2},\frac{1}{2},\ldots,\frac{1}{2}]$; call it
$H_{n}$.  Then each vertex of $H_{n}$ represents a model for $n$
variables.  The vertexes also represent assignments of probability 0
or 1 for the truth of each variable.  Every other point in $H_{n}$ can
be considered to give a probability on the interval $[0,1]$ for each
variable.   E.g., the center of $H_{n}$ represents a probability
assignment of 1/2 for each atom.

Next, consider a clause, $C_{i}$, of $S$ with $k_{i}$ literals.  Since
it 
is a disjunction, there is only one truth assignment over its literals
which makes it false: namely, where the atom of each literal is
assigned the value which makes the literal false.  However, every atom
not represented by a literal in $C_{i}$ 
can take on either truth value and not change the truth of the
clause.  Thus, there is a sub-hypercube of dimension $n-k_{i}$, that
is, a shifted, scaled instance of $H_{n-k_{i}}$, whose
vertexes are not solutions for $S$.  It turns out that there is an
$(n-1)$-dimensional hyperplane which can be constructed so as to separate
solutions from these non-solutions for $C_{i}$.  This chopping hyperplane
can be positioned anywhere along the edges connecting $H_{n-k}$ to the
rest of $H_{n}$.  Figure~\ref{fig:chop1} shows an example of chopping
one vertex, [1,0,1], from $H_{3}$.  The chop corresponds to finding
the intersection of $H_{n}$ with the set of points in the non-negative
half-space defined by the hyperplane.  Each conjunct provides a
corresponding half-space, and the set of all half-spaces, along with
$H_{n}$ are intersected to produce the feasible region for solutions.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
%\centering 
  \psfig{file=figures/Figg1.eps,width=5in,height=3in}  
%%    \includegraphics[width=2.8in]{figures/incoming}
  \caption{Example of Chopping [1;0;1] from $H_{3}$. The chopping
    hyperplane goes through the neighbors of $[1,0,1]$.}
  \label{fig:chop1}
\end{figure}

Once all the chops are made (i.e., the intersection of $H_{n}$ with
the non-negative 
half-spaces defined by the hyperplanes), the resulting convex set is
called the {\it feasible region}.  Note that it is necessary to
include hyperplanes which define the faces of $H_{n}$ in order to keep
the feasible region bounded.  Figure~\ref{fig:feasible} shows a simple
2-D example of the feasible region resulting from chopping off each corner.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/feasible.eps,width=5in,height=5in}  
%    \psfig{file=figures/feasible.eps,width=5in,height=3in}  
  \caption{Example 2-D Feasible Region Resulting from Chopping all
    Corners o $H_{2}$.}
  \label{fig:feasible}
\end{figure}
The hyperplanes in this case are lines in 2-D.  Each row provides the
coefficients $a,b,c$ of the standard form equation of a line:
$ax+by+c=0$:
\begin{verbatim}
   -0.7071   -0.7071    1.0607
   -0.7071    0.7071    0.3536
    0.7071   -0.7071    0.3536
    0.7071    0.7071   -0.3536
    1.0000         0         0
   -1.0000         0    1.0000
         0    1.0000         0
         0   -1.0000    1.0000
\end{verbatim} 
where the first four are the corner cuts, and the last four define
the faces (sides) of the square.  The chops are made midway along the
edges connecting the vertex to be removed and its neighbors.

\section{Solving SAT}

Given a feasible region, $\mathcal{F}$, corresponding to a CNF
sentence (or knowledge base), it is possible to probe that region to
determine if there is a SAT solution (i.e., a corner of $H_{n}$ in 
$\mathcal{F}$).  Note that the feasible region for any unsatisfiable
sentence has no point farther than $\frac{\sqrt{n-2}}{2}$ from the
center of $H_{n}$.  

Our approach takes advantage of the fact that the
Maximal Volume Inscribed Ellipsoid (MVE) of a full-dimensional convex
polytope defined by a finite set of affine inequalities can be found
in polynomial time \cite{Zhang2003}, and the MVE will, in general,  
have its major semi-axes aligned with the
most elongated parts of $\mathcal{F}$.  Moreover, Prof. Zhang 
provided us with a Matlab function which produces an ellipsoid
representation consisting of $x$ and $E$, where $x$ is the center of
the ellipsoid and $E$ is the matrix such that the points,
$\mathcal{P}$, of the ellipsoid are defined as:
\[ \mathcal{P} = \{ x + Es | s\in\Re^{n} \ni \Vert s\Vert\leq 1\}\]
The Singular Value Decomposition of $E$ yields the semi-major axes of
the MVE.  In order to increase the
volume, it is possible to move the hypercube face constraints outward
to allow a larger volume for the ellipsoid.  Figure~\ref{fig:ellipse2}
demonstrates this idea in 2-D where there is just one solution
([0;0]), and the sides of the square have been moved out 10 units.

\vspace{0.4in}
\begin{figure}[!htb]
%  \vspace{0.1in}
  \centering
    \psfig{file=figures/ellipse2.eps,width=5in,height=5in}  
  \caption{Example 2-D MVE Showing Major Semi-Axis in Direction of Solution.}
  \label{fig:ellipse2}
\end{figure}

To test the practicality of this approach, the following experiment
was performed:
\begin{itemize}

  \item
  A  set of 1000 random knowledge bases over 20 variables was
  generated.

  \item
  The corresponding feasible region was determined for each KB.

  \item
  The MVE was found for each feasible region.

  \item
  The major semi-axes were found.

  \item
  The feasible region boundary points along both directions of the
  major semi-axes were found.

  \item
  If any point was greater than $\frac{\sqrt{n-2}}{2}$ away from the
  center, then a solution is known to exist.
\end{itemize}
A solution was found in this way for every knowledge base.  Note that
this is only a heuristic and is not guaranteed to find a solution.  If
the Minimal Volume Circumscribing ellipsoid were found instead, then
this would guarantee a solution, but this problem is NP hard
\cite{Freund1985}.

To see how {\it Chop-SAT} relates to standard SAT solvers, consider
DPLL. DPLL is a complete backtracking search algorithm which as its
major step assigns a value to a variable, then determines if there is
a solution (i.e., it reduces the conjuncts, assigns necessary values
to resulting unit clause variables, and assigns values to pure
variables with only one polarity across all conjuncts).
{\it Chop-SAT} can be viewed as an alternative geometric approach to
this solution determination step only with no need, in general, to be
embedded in a complete search.

{\it Chop-SAT} represents the SAT problem as a convex feasible region
where if this region has a corner from the original n-D hypercube,
then a solution exists; if not, then the sentence is unsatisfiable.
{\it Chop-SAT} works by using linear programming (linprog in Matlab)
to find 
extremal vertexes by projecting the feasible region onto a selected
vector.  Let $\mathcal{F}$ be the feasible region of a CNF sentence;
then linear programming finds$x\in\mathcal{F}$ which minimizes
$f^{T}x$ such that $Ax\leq b$ and $lb\leq x \leq ub$, where $lb=0$ and
$ub=1$.

For example, if $f=[1,0,0]^{T}$ then the feasible region is projected
onto the $x$-axis (in 3-D).  Of course, {\it Chop-SAT} when embedded
in a search algorithm like DDLL is also complete, but we use it as a
one-step algorithm since this usually finds a solution.  Note that we
can also make {\it Chop-SAT} complete by projecting onto all the
diagonal axes of the n-D hypercube, but our original hope was that
geometry would provide a polynomial time solution.  {\it Chop-SAT} can
determine that a feasible region is from an unsatisfiable sentence
because of the following property: For every feasible region arising
from an unsatisfiable CNF sentence, there is no point at distance
greater than $\frac{\sqrt{n-1}}{2}$ from the center of the hypercube;
this means the feasible region can undergo any rotation about the
center of the hypercube and all points of the feasible region remain
within the bounds of the n-D hypercube -– this is not the case for
feasible regions containing solutions. 

\section{Solving for Atom Probabilities}

Another important problem for an agent is to determine the probability
of the state of the world.  For example, in the Wumpus World, the
agent will die if it enters a cell with a pit. Here we describe a
method to determine such probabilities using the feasible region
arising from a CNF sentence knowledge base.

For any given satisfiable knowledge base, the atom probabilities are
just the average of the 0/1 truth assignments of the models which make
satisfy the CNF sentence as described in the introduction.  However,
since it is too computationally costly to determine all possible
solutions and take their average, we propose the following 
approximations that can be found within a feasible region
$\mathcal{F}$:
\begin{itemize}

  \item
  the analytic center of $\mathcal{F}$.

  \item
  the p-center of $\mathcal{F}$.

  \item
  the center of the MVE.

  \item
  mean of samples from $\mathcal{F}$.
\end{itemize}

\vspace{0.2in}
\noindent
{\it Analytic Center of $\mathcal{F}$}

\vspace{0.1in}
\noindent
The {\it analytic center} of $\mathcal{F}$ is defined as:
\[ c = max_{y} \prod_{h}(a_{h} \cdot \left[ \begin{array}{c} y \\ 1 \end{array}\right]) \]
where $y\in \mathcal{F}$ and $a_{h}$ is the hyperplane coefficient
vector for hyperplane $h$.

\vspace{0.2in}
\noindent
{\it P-Center of $\mathcal{F}$}

\vspace{0.1in}
\noindent
The p-center of the feasible region is defined as follows
\cite{Moretti2003}: (1) choose 
an initial point $x\in\mathcal{F}$; (2) for each hyperplane constraint
find the line normal to the hyperplane which goes through $x$; (3)
find the two most distant points in $\mathcal{F}$ on this line; (4)
Average all the points found this way and assign the value to $x$; (5)
stop if $x$ does not change significantly.

\vspace{0.2in}
\noindent
{\it Chop-SAT Mean Center of $\mathcal{F}$}

\vspace{0.1in}
\noindent
In this approach, a number of samples are found in the feasible region
and their average determined.  For example, solve the following:
\[ min_{x} f^{T}x\]
such that $x\in \mathcal{F}$ and $f$ is taken as the positive and
negative unit vector along each axis of the n-D space.

\vspace{0.2in}
\noindent
{\it MVE Center of $\mathcal{F}$}

\vspace{0.1in}
\noindent
The MVE provides both the center of the MVE as well as the directions
of the semi-axes.  Here, the center of the MVE is used to approximate
the atom probabilities.

\subsection{Experimental Study}

For this study, 1000 random knowledge bases were generated with 5
atoms, a maximum of 10 clauses, and at most three literals in a
clause.  Figure~\ref{fig:CtrErr} shows the Euclidean distance between
the atom probability vector and the four proposed approximations: (1)
the analytic center (has lowest error), (2) the p-center (next lowest
error), (3) the Chop mean center (similar to p-center error), and (4)
the MVE center (has the most error).  The center errors over all trials
was 0.25, 0.52, 0.57, and 1.07, respectively.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/CtrErr.eps,width=5in,height=5in}  
  \caption{Error of Approximation Methods: Analytic Center (blue),
    P-Center (red), Chop center (mustard), MVE center (purple).}
  \label{fig:CtrErr}
\end{figure}

Figure~\ref{fig:CtrMass} shows how the centers cluster.  Since the
vectors are all 5-dimensional, they are converted to a 2-dimensional
representation which maintains spatial coherence.  As can be seen, the
analytic centers spread similarly to the actual atom probabilities,
the MVE centers form a tight central cluster, the p-centers skew
somewhat away (up) from the actual atom probabilities, while the Chop
mean centers skew a good bit away from the actual probabilities.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/CtrMass.eps,width=5in,height=5in}  
  \caption{The center distributions.}
  \label{fig:CtrMass}
\end{figure}
The experiments indicate that the Analytic Center is the best
approximation to the actual atom probabilities.

\section{Wumpus World Experiment}

To demonstrate the effectiveness of this approach, agent decision
making was tested in the Wumpus World framework.  Wumpus World was
proposed by Yob \cite{Yob1975}, and has been used as a standard agent
testbed for some time \cite{Russell2010}.  Wumpus world here is a 4x4
grid of cells; each 
cell may contain a pit with 20\% probability, and if there is a pit it
is the only thing in the cell.  One cell contains some gold, and one
cell contains a Wumpus (the gold may be co-located with the Wumpus).
An agent starts in cell $(1,1)$ and explores the grid in order to find
the gold.  Each cell neighboring a pit has a breeze, and each cell
neighboring the Wumpus has a stench.  Figure~\ref{fig:Wumpus} shows an
example board with the agent in cell $(1,1)$ with direction
$\theta=0$, with pits in cells $\{(1,4),(4,2),(4,3)\}$, the Wumpus in
cell $(2,3)$, and the gold in cell $(4,4)$.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/Wumpus.eps,width=5in,height=5in}  
  \caption{An Example Wumpus World Board.}
  \label{fig:Wumpus}
\end{figure}

The agent has a set of percepts
in a cell (represented as bits): (1) stench, (2) breeze, (3) glitter,
(4) bump, and (5) scream.  The glitter percept lets the agent know
it's in the cell with the gold.  The agent has a state $(x,y,\theta)$,
where $(x,y)$ is its location in the grid, and $\theta$ is its
orientation $\theta\in\{0,90,180,270\}$ degrees.  The agent has a set
of possible actions: (1) rotate left, (2) rotate right, (3) forward,
(4) grab, (5) shoot, and (6) climb.  If the agent moves into a cell
with a pit or the Wumpus, it dies.  The agent has one arrow and can
shoot the Wumpus.

The agents here all share a Belief, Desire, Intention cognitive
architecture \cite{Georgeff1999}.
The Belief-Desire-Intention architecture is a hierarchical
organization of states and actions (grouped into plans) 
that was designed specifically for agent models. The architecture not
only defines the conceptual structure of a program, 
but also a process structure that enables dynamic planning.
Organizing the program in this way supports both
reasoning by the autonomous agent as well as reasoning by
human operators. The structure of desires, intentions, beliefs,
and plans coincides well with the reasoning of the human
operator. For example, a human observer could ask a BDI
agent directly, ``What is your current plan?'' and the agent could
respond ``Located the Wumpus and pro ceding to kill it.''

In the specific scenario here, the desires are: (1) escape, (2) kill
the Wumpus, and (3)
explore.  If it has the gold, its intention will be to escape with the
gold.  The agent's intention will be to kill the Wumpus if its
location is known.  Otherwise, its intention is to explore the grid.
In order to explore, the agent selects the lowest probability risk
unvisited cell.  All agents have the same BDI architecture and only
differ in how they compute the probabilities for risk: (1) a human
produced algorithm to assign pit and Wumpus probabilities, (2) the
analytic center, (3) {\it Chop-SAT} mean, and (4) Monte Carlo
simulation based on statistics over sample boards satisfying the known
percept information.

The experimental method is to generate 1,000 random Wumpus boards, run
each agent type on the boards, and measure successful escape with the
gold.  Note that the Monte Carlo results will be very close to optimal
and serves as the upper bound on success.  The results are given in
Table 1.  As can be seen, the {\it Chop-SAT} based agent performed the
best, and this is a good indication of its efficacy.

\vspace{0.2in}
\begin{center}
Table 1. Results of Wumpus World Experiment.

\begin{tabular}{|l|l|l|l|l|} \hline
{\bf Number} & {\bf Human} & {\bf Analytic} & {\bf Chop-SAT} & {\bf Monte
Carlo} \\ 
{\bf of Boards} &  & {\bf Center} & & \\ \hline
1000 & 585 & 598 & 608 & 613.3 \\ \hline
\end{tabular} 
\end{center}

These experiments from Wumpus world have 80 logical variables (i.e.,
$2^{80}$ models for the knowledge base!).  The point is to see if the
probabilistic method provides adequate variable probabilities to help
make good (life preserving) decisions.  The baseline of the experiment
is given as the Monte Carlo method for determining these probabilities
(i.e., random boards are generated that satisfy the knowledge acquired
during a game and the exact variable probabilities are estimated from
these board configurations).  The overall statistic is that 1000
random Wumpus boards are generated, and each algorithm (human,
analytic center, {\it Chop-SAT}) is compared to the ground truth
approximated by the Monte Carlo method.  Thus, there are three solvers
(humans wrote programs to assign probabilities, the analytic center
method provides probabilities, and {\it Chop-SAT} provides
probabilities) which are then used to make decisions.  Other
probabilistic SAT solution methods were not used because they are all
exponential complexity and either won’t run on this size problem or
require max entropy type assumptions which are not valid here. 

A current application under study is the use {\it Chop-SAT} as part of
a Belief-Desire-Intention architecture for autonomous Unmanned
Aircraft Systems agents \cite{Sacharny2021}.  We are conducting
experiments this summer at the US Air Force Academy where such an
architecture for decision making is used.

\section{Non-Euclidean Geometry Approach}

The Euclidean method described above shows how each disjunction in the
CNF sentence gives rise to a hyperplane which separates the
non-solution vertexes (on the negative side of the hyperplane) of
$H_{n}$ from the 
solution vertexes (on the non-negative side of the hyperplane); i.e.,
the intersection 
of the non-negative half-spaces of these hyperplanes results in a
convex feasible region which must contain any solution which exists.
The non-Euclidean method projects $H_{n}$ onto the
$n$-dimensional unit hypersphere considered as an $n$-dimensional
Poincar\'{e} Disk (see \cite{Henderson2023a}).  The advantage of this
approach is that the
vertexes of $H_{n}$ are mapped onto the surface of the disk and are
thus at infinite distance (in terms of hyperbolic geometry) from the
center of the disk.  The idea is that this property makes the
solutions more readily identifiable.

The motivation for using non-Euclidean geometry is that it allows us
to put the solutions at a unique location: at infinite distance from
the origin in terms of non-Euclidean distance). That is, SAT is mapped
onto the Poincare Disk as follows (see Figure~\ref{fig:Eu2PD}).
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/Eu2PD.eps,width=5in,height=5in}  
%    \includegraphics[width=2.8in]{figures/Eu2PD}
  \caption{The Vertexes of the Hypercube are Projected onto the Hypersphere.}
  \label{fig:Eu2PD}
\end{figure}
The corners of the $n$-dimensional hypercube are projected onto the
$n$-dimensional hypersphere, $D_{n}$, as ideal points (i.e., points on
the surface of the hypersphere - note that these are not points in the
Poincar\'{e} Disk).  These ideal points are an infinite distance from
the center of the unit hypersphere.  Unlike in Euclidean geometry
where the hyperplane chops usually produce a bounded convex polytope
for the feasible region whether or not a solution exists, in the case
of the Poincar\'{e} Disk representation, the feasible region is only
bounded when no solution is in the feasible region.  Given this fact,
the goal is to find low-complexity algorithms to determine whether or
not there exists a sequence of points in the feasible region such that
in the limit their distance from the origin is infinite (in hyperbolic
geometry).
%\begin{equation*}
%\begin{aligned}
%L=\frac1 2M_1{L_1}^2{\dot{\theta_1}^2 }+
%\frac1 2M_2\left[L_1^2{\dot{\theta_1}^2+L_2^2{\dot{\theta_2}^2} +
%2L_1L_2{\dot{\theta_1}{\dot{\theta_2}}}cos({{{\theta_1-\theta_2)}}}}\right]
%\\ + (M_1+M_2)gL_1cos{\theta_1}+M_2gL_2cos{\theta_2}
%\end{aligned}
%\end{equation*}

The goal is to provide a representation in terms of the Poincar\'{e}
Disk which allows the solution vertexes to be found through efficient
geometric algorithms.  To set up this representation, a few basic
facts concerning the Poincar\'{e} Disk geometry must be defined.

\subsection{Poincar\'{e} Disk Distance}

Consider the 2-dimensional Poincar\'{e} Disk (Figure~\ref{fig:PD2D},
upper left circle).
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/PD2D.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/PD2D}
  \caption{The 2D Poincar\'{e} Disk; $L_{1}$ is a line through the
    center, $\mathcal{O}=(0,0)$, i.e., a diameter; $L_{2}$ is a
    circular arc which is orthogonal to the unit circle.}
  \label{fig:PD2D}
\end{figure}
The distance between two points, $p$ and $q$, in the Poincar\'{e} Disk
is defined in terms of Euclidean distance on points given as complex
numbers:
\[d(p,q) = ln(\frac{|ap||qb|}{|aq||pb|})\]
where $a$ and $b$ are the intersection points with the unit circle of
the unique circle (Figure~\ref{fig:PD2D}, lower right circle) through
$p$ and $q$ which is orthogonal to the unit 
circle.  Moreover, the points are arranged in the order $a$, $p$, $q$
and $b$ along the circle.  An alternative formulation which does not
require the orthogonal circle is given by:
\[d(p,q) = acosh(1 + \frac{2|pq|^{2}|r|^2}{(|r|^2-|op|^2)(|r|^2-|oq|^2)})\]
where $r=1$ for the unit disk, and $|op|$ and $|oq|$ are the Euclidean
distances of $p$ and $q$ from the origin, respectively.

\subsection{The Orthogonal Circle through Two Points}

The angle between two circles (defined in Euclidean coordinates) is
given by:
\[cos(\theta) = \frac{r_{1}^{2} + r_{2}^{2} - \Vert C_{1}-C_{2} \Vert^{2}}{2r_{1}r_{2}}\]
where $r_{1}$ is the radius of the first circle, $r_{2}$ the radius of
the second circle, and $C_{1}$ and $C_{2}$ are the centers of the two
circles.  Two circles are said to be orthogonal if
$\theta=\frac{\pi}{2}$.

Given two points, $p$ and $q$, in the Poincar\'{e} Disk, the straight
line (in hyperbolic terms)
through them can be found as follows.  If $p$ and $q$ lie on a
diameter of the Poincar\'{e} Disk, then the line is just the straight
Euclidean line through the two points.  This can be viewed as a circle
of infinite radius through the two points.  If $p$ and $q$ do not lie
on a diameter line, then there are two circles to consider: the unit
disk with $r_{1}=1$ and $C_{1}=(0,0)$, and the circle through $p$ and
$q$ with radius $r_{2}$ and center $C_{2} = (C_{x},C_{y})$.  Since the
circles are orthogonal:
\[cos(\theta)=cos(\frac{\pi}{2})= 0\]
\[\Rightarrow 0 = 1 + r_{2}^{2} - \Vert C_{2}\Vert ^{2}\]
\[\Rightarrow r_{2}^{2} = C_{x}^{2} + C_{y}^{2} - 1\]

Each point, $p$ and $q$, gives rise to another equation; e.g., for $p$:
\[r_{2}^{2} = (p_{x}-C_{x})^2 + (p_{y}-C_{y})^2\]
\[\Rightarrow r_{2}^{2} = p_{x}^{2} -2p_{x}C_{x} + C_{x}^2 + p_{y}^{2}
-2p_{y}C_{y} + C_{y}^2\]
and substituting the first into the second:
\[C_{x}^{2}+C_{y}^{2}-1 = C_{x}^{2}+C_{y}^{2}-2p_{x}C_{x}-2P_{y}C_{y}+p_{x}^{2}+p_{y}^{2}\] 
\[\Rightarrow p_{x}C_{x} + p_{y}C_{y} = \frac{p_{x}^{2}+p_{y}^{2}+1}{2}\]
Likewise:
\[\Rightarrow q_{x}C_{x} + q_{y}C_{y} = \frac{q_{x}^{2}+q_{y}^{2}+1}{2}\]
This can be solved as a linear system:\\
\vspace{0.1in}
$A = \begin{bmatrix}
    p_{x} & p_{y} \\
    q_{x} & q_{y} 
\end{bmatrix}$
$b = \begin{bmatrix}
   \frac{p_{x}^{2} + p_{y}^{2} + 1}{2}\\
   \frac{q_{x}^{2} + q_{y}^{2} + 1}{2}
\end{bmatrix}$
and solving for the center, $C$:
\[AC = b\]
Finally, the radius is found as follows:
\[ r = \Vert C-p \Vert\]

\subsection{Representation of Bounding Faces in the Poincar\'{e} Disk}

In Euclidean geometry, the SAT problem is posed in terms of removing
vertexes from the hypercube.  Each conjunct in the CNF sentence
provides a hyperplane which divides the feasible region from the
non-satisfying solutions for that conjunct.  However, in the
Poincar\'{e} Disk, a way must be found to represent the original
complete set of vertexes, and then some way to chop non-solutions from
the feasible region.  One way to go at this is to use a square like
the one shown in Figure~\ref{fig:square}.  The problem arises that
this is likely to suffer from the same problem as the Euclidean
representation, namely that a projection does not readily reveal
solution corners.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/square.eps,width=5in,height=5in}  
%    \includegraphics[width=2.8in]{figures/square}
  \caption{Representing the Complete Feasible Region as a Square in
    the Poincar\'{e} Disk. The left side is the complete feasible
    region, while the right side shows the feasible region when
    $(0,1)$ is not a truth assignment that satisfies the CLF sentence.}
  \label{fig:square}
\end{figure}

Another representation that may allow lower complexity discovery of
whether a solution exists or not is given by the feasible region shown
in Figure~\ref{fig:squareinf}.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/squareinf.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/squareinf}
  \caption{Representing the Complete Feasible Region as a Square with
    corners at infinity in the Poincar\'{e} Disk.}
  \label{fig:squareinf}
\end{figure}
The $2n$ $(n-1)$-dimensional bounding faces of the hypercube are
represented in the Poincar\'{e} Disk in terms of hyperspheres through
the corresponding face vertexes.  The centers of these hyperspheres
will lie along 
the coordinate axes (one each in the positive and negative
directions).  Let $v_{1}$ be the unit vector from the center of
$D_{n}$ to a vertex of the face, and $v_{2}$ be the unit vector in the
desired axis direction.  We seek the center, $C$ and radius $r$ of the
hypersphere through the face vertexes. Given that the desired
hypersphere is orthogonal to the unit disk, then the angle, $\theta$,
between $v_{1}$ and $v_{2}$ is given by:
\[ \theta = acos(v_{1}\cdot v_{2})\]
which means that the distance, $xd$, along the axis from the origin to $C$
is:
\[xd = \frac{1}{cos(\theta)}\]
which gives $C$.  This process is done for the $2n$ bounding face
constraints on the feasible region.

\subsubsection{Clause Chops}

As has been described, {\it lines} in the Poincar\'{e} Disk are
circular arcs when viewed in Euclidean geometry, and this allows
non-solution vertexes to be separated from the feasible region by
choosing the appropriate side of the circle which defines the chop.
What is required is an algorithm to convert from a CNF conjunct to the
equation of a circle which has the non-solutions on one side and the
remaining possible solutions on the other.  This algorithm is provided
below.

Given clause:
\[C = L_{1}\vee L_{2}\vee \ldots \vee L_{k}\]
convert to $V = [v_{1},v_{2},\ldots,v_{n}]$ where $n$ is the number of
atoms, and $a_{i}$ is the $i^{th}$ atom:
\[ v_{i} = -1 \textit{ if }\exists j\ni\neg a_{i}=L_{j}\]
\[ v_{i} = 0 \textit{ if no literal of }a_{i}\in C\]
\[ v_{i} = 1 \textit{ if }\exists j \ni a_{i}=L_{j}\]
Let $\alpha = -V$ and $u_{\alpha} = \frac{a}{\Vert \alpha \Vert}$.
Obtain an $H_{n}$ vertex to be chopped 
by substituting -1 for 0's, if any, in $\alpha$:
$chop\_pt = \alpha_{-1\leftarrow 0}$.

Obtain a non-chopped neighbor, $nei\_pt$, by inverting a non-zero
element of $chop\_pt$.

Obtain the projection point by sliding along an $H_{n}$ edge
connecting the $chop\_pt$ to the $nei\_pt$ by the desired percentage
amount $\Delta\in(0,1]$; that is:
\[proj\_pt = (1-\Delta)chop\_pt + \Delta nei\_pt\]

To get the projection point on the Poincar\'{e} Disk boundary:
\[proj\_pt\_PD = \frac{proj\_pt}{\Vert proj\_pt\Vert}\]

Then:
\[ \theta = acos(u_{a}\cdot proj\_pt\_PD)\]
\[d = \frac{1}{cos(\theta)}\]
\[r_{2} = \sqrt{d^{2}-1}\]
\[C = du_{a}\]

Consider the following example.  Let $C = \neg A \vee \neg B$.  Then
$V = [-1,-1]$, $\alpha = [1,1]$, and $\mu_\alpha = [0.7071,0.7071]$.
Then $chop\_pt = [1,1]$ and $nei\_pt = [-1,1]$.  Let $\Delta = 0.9$,
then $proj\_pt = [-0.8,1]$ and $proj\_pt\_PD = [-0.6247,0.7809]$
resulting in $\theta = 1.4601$ radians (83.66 degrees), and $d =
9.0554$.

Notice that if single-literal clauses are allowed, then the center of
the chop hypersphere may flip sides to 
satisfy circle orthogonality.  If so, the feasible side of the
hypersphere is the interior. Such clauses can be avoided by deleting
the atom of the literal and substituting its truth value into the
other clause where it appears and then reducing these clauses
accordingly.
 Figure~\ref{fig:chops} shows example 2D
and 3D chops.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/chops.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/chops}
  \caption{Examples of Chops in 2D and 3D.}
  \label{fig:chops}
\end{figure}
Note that this formulation works in any dimension.

The $\Delta$ parameter determines how far the chop occurs from the
non-solution vertexes which are being cut.  Figure~\ref{fig:del} shows
some example positions for chops.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/del.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/del}
  \caption{The Impact of $Delta$ on Chop Distance from Non-Solution Vertexes.}
  \label{fig:del}
\end{figure}
Figure~\ref{fig:MPchop} shows the chops for Modus Ponens,
Figure~\ref{fig:edgesChop} shows three edges chopped, and
Figure~\ref{fig:faceChop} shows a 3D face chop.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/MPchop.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/MPchop}
  \caption{Chops for Modus Ponens.}
  \label{fig:MPchop}
\end{figure}
\begin{figure}![tbh]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/edgesChop.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/edgesChop}
  \caption{Three Edges Chop.}
  \label{fig:edgesChop}
\end{figure}
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/faceChop.eps,width=5in,height=5in}
%    \includegraphics[width=2.8in]{figures/faceChop}
  \caption{3D Face Chop.}
  \label{fig:faceChop}
\end{figure}

\subsection{Method}

Given a CNF sentence, the problem solution is found as follows:
\begin{itemize}

  \item
  A set of chops are produced for the CNF clauses; these chops are
  hyperplanes just like those used in Euclidean geometry.  Note that
  they can also be viewed as infinite radius hyperspheres through
  those neighbor vertexes, however, these hyperspheres are not
  orthogonal to the unit disk.

  \item
  In addition to the constraint surfaces arising from the chopped
  vertexes, it is also necessary to bound the feasible region to be
  interior to the transformed unit cube.  To this end, a set of face
  constraint hyperspheres are added; these hyperspheres are
  orthogonal to the unit disk. 

  \item
  A Barrier Method type algorithm is developed for this constraint set
  which moves in the selected projection direction (i.e., maximizes
  the projection) using the
  hypersphere surfaces as barrier constraints.  This is implemented as
  a force field method and is described in detail below.  Other forces
  may also be introduced to ameliorate the convergence; e.g., a force
  away from the origin.

  \item
  A solution is considered to exist if the convergence point is close
  enough to a solution vertex; i.e., in the limit, the distance from
  the origin of the points in the sequence grows without limit.
\end{itemize}
In Euclidean geometry, existing software tools exist to solve linear
programming problems (e.g., the Matlab function {\it linprog}).
However, a variant was implemented here to handle the mix of hyperplane and
hypersphere surfaces.

\subsubsection{Barrier Method}

The Barrier Method is formulated as a force field problem as described
by Boyd and Vandenberg \cite{Boyd2021}.  For each point $x\in
\mathcal{F}$, a barrier force is defined for each constraint surface:
\[F_{i}(x) = \nabla(-log(-f_{i}(x)))=\frac{\nabla f_{i}(x)}{f_{i}(x)}\]
where $F_{i}(x)$ is the force vector at point $x$ from the $i^{th}$
constraint, and $f_{i}(x)$ is the (minimal) distance function from $x$
to the $i^{th}$ constraint surface.
The projection constraint force (called the forcing direction force)
is:
\[ F_{0}(x) = -t\nabla f_{0}(x)\]
where $F_{0}(x)$ is the forcing direction force at $x$ and $f_{0}(x)$
is $f^{T}x$ where $f$ is the direction of the forcing vector.

These forces are based on the logarithmic (barrier) function:
\[ \Phi(x) = -\sum_{i=1}^{m} log(-f_{i}(x))\]
and the distance function for hyperplanes is:
\[ f_{i}(x) = a_{i}^{T}x + c_{i}\]
and for hyperspheres:
\[ f_{i}(x) = \Vert C_{i}-x\Vert - |r_{i}|\]
where $C_{i}$ and $r_{i}$ are the center and radius, respectively, of
the hypersphere.
Then the force field model is defined in terms of forces generated by
the minimization impulse function (to move in a certain direction) and
the repulsive force of the constraint surfaces.  Boyd gives the
hyperplane forces which in our representation are:
\[F_{i}(x) = \frac{-a_{i}}{b_{i}-a_{i}^{T}x}\]
\[F_{0}(x) = tf\]
The hypersphere forces are derived as follows:
\[f_{0}(x) = f^{T}x = \sum_{i=1}^{n} f(i)x(i)\]
Therefore:
\[\nabla f_{0}(x) = 
  \left[ 
    \begin{array}{c}
      \frac{\partial f_{0}}{\partial x_{1}} \\
      \frac{\partial f_{0}}{\partial x_{2}} \\
      \cdots    \\
      \frac{\partial f_{0}}{\partial x_{n}}
    \end{array}
  \right] 
  = \left[
      \begin{array}{c}
         f(1) \\
         f(2) \\
         \cdots \\
         f(n)
      \end{array}
    \right]
  = f
\]
which implies that:
\[F_{0}(x) = tf\]
In addition:
\[ f_{i}(x) = ((C(1)-x(1))^{2} + \cdots + (C(n)-x(n))^{2})^{1/2} -
r_{i}\]
which means that:
\[ \frac{\partial f_{i}(x)}{\partial x_{j}} =
\frac{1}{2}((C_{i}(j)-x(j))^{2})^{-1/2}(2(C_{i}(j)-x(j)))(-1) =
\frac{x(j)-C_{i}(j)}{\Vert C_{i}-x \Vert}\]
and finally:
\[\nabla f_{i}(x) = \frac{x-C_{i}}{\Vert C_{i}-x\Vert}\]
and
\[F_{i}(x) = \frac{x-C_{i}}{\Vert C_{i}-x\Vert(\Vert C_{i}-x\Vert - r_{i})}\]
In order to encourage moving toward the disk boundary, another forcing
function may be defined as:
\[F_{b}(x) = \frac{t_{b}x}{\Vert x\Vert}\]
where $t_{b}$ is a magnitude value.

Given $x\in \mathcal{F}, t^{(0)}>0, \mu>1, \epsilon>0$, then the
Barrier Method is:

\vspace{0.1in}
\noindent
{\bf repeat}
\begin{enumerate}

  \item
  Centering step: find force equilibrium point $x^{*}(t)$ of
  $tf_{0}+\Phi$

  \item
  Update: Set $x$ to $x^{*}(t)$

  \item
  Stopping Criterion: {\bf quit} if $\mu/t<\epsilon$

  \item
  Increase $t$: Set $t$ to $\mu t$
\end{enumerate}

Figure~\ref{fig:BMForces2D} shows the forces resulting from only
constraint surfaces repulsion forces (left), an upward external force
(middle), and a downward external force (right).  The basic approach
is to use the origin as an initial starting point since the origin is
guaranteed to be in the feasible region, and find the equilibrium point
when no force is applied (this corresponds to the analytic center).
Next, starting from the analytic center and using a forcing direction,
follow the resultant forces and move to the equilibrium point for this
set of forces.  Choosing different forcing directions results in an
exploration of the feasible region.  The problem is to determine an
effective and efficient search strategy.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/BMForces2D.eps,width=5in,height=5in}
%    \includegraphics[width=4in]{figures/BMForces2D}
  \caption{Example Force Fields: Only constraint surface repulsion
    forces are present (left); An added upward force (middle); A
    downward external force (right).}
  \label{fig:BMForces2D}
\end{figure}

Figure~\ref{fig:Barrier2D3Sols} shows the Barrier Method applied to
finding solutions for a 2D problem with three solutions.
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/Barrier2D3Sols.eps,width=5in,height=5in}
%    \includegraphics[width=4in]{figures/Barrier2D3Sols}
  \caption{The Paths for the Barrier Method finding Solutions in a 2D Problem.}
  \label{fig:Barrier2D3Sols}
\end{figure}
\begin{figure}[!htb]
  \vspace{0.1in}
  \centering
    \psfig{file=figures/path3D111v2.eps,width=5in,height=5in}
%    \includegraphics[width=4in]{figures/path3D111v2}
  \caption{The Paths for the Barrier Method finding a Solution in a 3D Problem.}
  \label{fig:path3D111v2}
\end{figure}
A 3-D example path is shown in Figure~\ref{fig:path3D111v2}.

\section{Conclusions and Future Work}

The results of the experiments indicate that this geometric approach
works well at least up to dimension 20, and that the analytic center
is the best approximation to the actual atom probabilities on a random
set of knowledge bases.  However, the probabilities provided by the
{\it Chop-SAT} method performed slightly better in the decision making
experiment in Wumpus World, and both the analytic center and {\it
  Chop-SAT} methods performed better than a human developed risk
probability algorithm.  Moreover, the non-Euclidean geometry also
allows the determination of solutions, although since the barrier
method is applied to a non-convex set, it is not guaranteed to find a
vertex solution.

In the future, work will be performed in order to:
\begin{itemize}

  \item
  test the SAT solver experiments in higher dimensions,

  \item
  seek effective ways to exploit the non-Euclidean geometry
  representation; e.g., view the feasible region as a domain to be
  explored by a geo-bot which has a set of range sensors to help it
  detect feasible points far from the Poincar\'{e} disk origin.

  \item
  use the atom probability approximation in more complex agent
  decision making situations (e.g., UAS traffic management) and
  compare its effectiveness with other methods.

  \item
  use the method as the basis for decision-making in a set of
  autonomous Unmanned Aircraf Systems (UAS) agents,

  \item
  explore formal verification of the BDI method.
\end{itemize}

\vspace{0.5in}
\noindent
{\large\bf Acknowledgements}

\noindent
This work was supported in part by National Science Foundation award
2152454.


%% The Appendices part is started with the command \appendix;
%% appendix sections are then done as normal sections
%% \appendix

%% \section{}
%% \label{}

%% If you have bibdatabase file and want bibtex to generate the
%% bibitems, please use
%%
%%  \bibliographystyle{elsarticle-num} 
%%  \bibliography{<your bibdatabase>}

%% else use the following coding to input the bibitems directly in the
%% TeX file.

%%%%%\begin{thebibliography}{00}

%% \bibitem{label}
%% Text of bibliographic item

%%%%%\bibitem{}

%%%%%\end{thebibliography}
\bibliography{RAS}
\end{document}
\endinput
%%
%% End of file `elsarticle-template-num.tex'.
