Boolean satisfiability (SAT) reduction for geometry and kinematics agnostic multi-agent planning

A computing device, comprising:

• one or more processors;
• and
• data storage including at least computer-executable instructions stored thereon that, when executed by the one or more processors, cause the computing device to perform functions comprising:
• receiving a roadmap representing a plurality of paths through an environment;
• discretizing the roadmap to obtain a discrete planning graph, wherein the discrete planning graph comprises a plurality of states corresponding to discretized path segments of the plurality of paths of the roadmap such that states corresponding to adjacent discretized path segments are connected in the discrete planning graph;
• determining a Boolean equation representing at least a portion of the discrete planning graph, wherein the Boolean equation comprises a plurality of Boolean clauses, wherein the plurality of Boolean clauses comprise a plurality of Boolean variables, wherein each Boolean variable of the plurality of Boolean variables represents a possible state of a robotic device in the discrete planning graph at one of a plurality of times;
• determining a set of values comprising a value of true or false for each Boolean variable of the plurality of Boolean variables, wherein the set of values satisfies the Boolean equation, wherein the set of values indicates a sequence of states for the robotic device to occupy from the plurality of states of the discrete planning graph, and wherein the sequence of states for the robotic device to occupy is represented by Boolean variables having a determined value of true;
• and
• providing a route through the environment for the robotic device based on the determined sequence of states to cause the robotic device to occupy each state in the sequence of states over the plurality of times.

A non-transitory computer readable medium having stored thereon instructions, that when executed by one or more processors of a computing device, cause the computing device to perform functions comprising:

• receiving a roadmap representing a plurality of paths through an environment;
• discretizing the roadmap to obtain a discrete planning graph, wherein the discrete planning graph comprises a plurality of states corresponding to discretized path segments of the plurality of paths of the roadmap such that states corresponding to adjacent discretized path segments are connected in the discrete planning graph;
• determining a Boolean equation representing at least a portion of the discrete planning graph, wherein the Boolean equation comprises a plurality of Boolean clauses, wherein the plurality of Boolean clauses comprise a plurality of Boolean variables, wherein each Boolean variable of the plurality of Boolean variables represents a possible state of a robotic device in the discrete planning graph at one of a plurality of times;
• determining a set of values comprising a value of true or false for each Boolean variable of the plurality of Boolean variables, wherein the set of values satisfies the Boolean equation, wherein the set of values indicates a sequence of states for the robotic device to occupy from the plurality of states of the discrete planning graph, and wherein the sequence of states for the robotic device to occupy is represented by Boolean variables having a determined value of true;
• and
• providing a route through the environment for the robotic device to cause the robotic device to occupy each state in the sequence of states over the plurality of times.