-
Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs
Authors:
Hariprasadh Govindasamy,
Babak Esfandiari,
Paulo Garcia
Abstract:
We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (BCP) through fine-grained FPGA parallelism. Unlike prior state-of-the-art solutions, our solver eliminates costly clause look-up operations by assig…
▽ More
We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (BCP) through fine-grained FPGA parallelism. Unlike prior state-of-the-art solutions, our solver eliminates costly clause look-up operations by assigning clauses directly to clause processors on the FPGA and dividing large formulas into smaller partitions manageable by FPGA. Partitions are hot-swapped during runtime as required and the supported formula size is limited only by available external memory, not on-chip FPGA memory. We evaluate our solver on a Xilinx Zynq platform with results showing quicker execution time across various formula sizes, subject to formula partitioning strategy. Compared to prior state-of-the-art, we achieve 1.7x and 1.1x speed up on BCP for 2 representative benchmarks and up to 6x total speedup over software-only implementation.
△ Less
Submitted 13 April, 2024; v1 submitted 14 January, 2024;
originally announced January 2024.
-
FPGAs (Can Get Some) SATisfaction
Authors:
Hariprasadh Godindasamy,
Babak Esfandiari,
Paulo Garcia
Abstract:
We present a hardware-accelerated SAT solver suitable for processor/Field Programmable Gate Arrays (FPGA) hybrid platforms, which have become the norm in the embedded domain. Our solution addresses a known bottleneck in SAT solving acceleration: unlike prior state-of-the-art solutions that have addressed the same bottleneck by limiting the amount of exploited parallelism, our solver takes advantag…
▽ More
We present a hardware-accelerated SAT solver suitable for processor/Field Programmable Gate Arrays (FPGA) hybrid platforms, which have become the norm in the embedded domain. Our solution addresses a known bottleneck in SAT solving acceleration: unlike prior state-of-the-art solutions that have addressed the same bottleneck by limiting the amount of exploited parallelism, our solver takes advantage of fine-grained parallelization opportunities by hot-swapping FPGA clause assignments at runtime. It is also the first modern completely open-source SAT accelerator, and formula size is limited only by the amount of available external memory, not by on-chip FPGA memory. Evaluation is performed on a Xilinx Zynq platform: experiments support that hardware acceleration results in shorter execution time across varying formula sizes, subject to formula partitioning strategy. We outperform prior state-of-the-art by 1.7x and 1.1x, respectively, for 2 representative benchmarks, and boast up to 6x performance increase over software-only implementation.
△ Less
Submitted 18 December, 2023;
originally announced December 2023.
-
Toward Campus Mail Delivery Using BDI
Authors:
Chidiebere Onyedinma,
Patrick Gavigan,
Babak Esfandiari
Abstract:
Autonomous systems developed with the Belief-Desire-Intention (BDI) architecture are usually mostly implemented in simulated environments. In this project we sought to build a BDI agent for use in the real world for campus mail delivery in the tunnel system at Carleton University. Ideally, the robot should receive a delivery order via a mobile application, pick up the mail at a station, navigate t…
▽ More
Autonomous systems developed with the Belief-Desire-Intention (BDI) architecture are usually mostly implemented in simulated environments. In this project we sought to build a BDI agent for use in the real world for campus mail delivery in the tunnel system at Carleton University. Ideally, the robot should receive a delivery order via a mobile application, pick up the mail at a station, navigate the tunnels to the destination station, and notify the recipient.
We linked the Robot Operating System (ROS) with a BDI reasoning system to achieve a subset of the required use cases. ROS handles the low-level sensing and actuation, while the BDI reasoning system handles the high-level reasoning and decision making. Sensory data is orchestrated and sent from ROS to the reasoning system as perceptions. These perceptions are then deliberated upon, and an action string is sent back to ROS for interpretation and driving of the necessary actuator for the action to be performed.
In this paper we present our current implementation, which closes the loop on the hardware-software integration, and implements a subset of the use cases required for the full system.
△ Less
Submitted 22 July, 2020;
originally announced July 2020.
-
The Requirement Gatherers' Approach to the 2019 Multi-Agent Programming Contest Scenario
Authors:
Michael Vezina,
Babak Esfandiari
Abstract:
The 2019 Multi-Agent Programming Contest (MAPC) scenario poses many challenges for agents participating in the contest. We discuss The Requirement Gatherers' (TRG) approach to handling the various challenges we faced -- including how we designed our system, how we went about debugging our agents, and the strategy we employed to each of our agents. We conclude the paper with remarks about the perfo…
▽ More
The 2019 Multi-Agent Programming Contest (MAPC) scenario poses many challenges for agents participating in the contest. We discuss The Requirement Gatherers' (TRG) approach to handling the various challenges we faced -- including how we designed our system, how we went about debugging our agents, and the strategy we employed to each of our agents. We conclude the paper with remarks about the performance of our agents, and what we should have done differently.
△ Less
Submitted 4 June, 2020;
originally announced June 2020.
-
Behavior Cloning in OpenAI using Case Based Reasoning
Authors:
Chad Peters,
Babak Esfandiari,
Mohamad Zalat,
Robert West
Abstract:
Learning from Observation (LfO), also known as Behavioral Cloning, is an approach for building software agents by recording the behavior of an expert (human or artificial) and using the recorded data to generate the required behavior. jLOAF is a platform that uses Case-Based Reasoning to achieve LfO. In this paper we interface jLOAF with the popular OpenAI Gym environment. Our experimental results…
▽ More
Learning from Observation (LfO), also known as Behavioral Cloning, is an approach for building software agents by recording the behavior of an expert (human or artificial) and using the recorded data to generate the required behavior. jLOAF is a platform that uses Case-Based Reasoning to achieve LfO. In this paper we interface jLOAF with the popular OpenAI Gym environment. Our experimental results show how our approach can be used to provide a baseline for comparison in this domain, as well as identify the strengths and weaknesses when dealing with environmental complexity.
△ Less
Submitted 23 February, 2020;
originally announced February 2020.
-
Processing Regular Path Queries on Arbitrarily Distributed Data
Authors:
Alan Davoust,
Babak Esfandiari
Abstract:
Regular Path Queries (RPQs) are a type of graph query where answers are pairs of nodes connected by a sequence of edges matching a regular expression. We study the techniques to process such queries on a distributed graph of data. While many techniques assume the location of each data element (node or edge) is known, when the components of the distributed system are autonomous, the data will be ar…
▽ More
Regular Path Queries (RPQs) are a type of graph query where answers are pairs of nodes connected by a sequence of edges matching a regular expression. We study the techniques to process such queries on a distributed graph of data. While many techniques assume the location of each data element (node or edge) is known, when the components of the distributed system are autonomous, the data will be arbitrarily distributed. As the different query processing strategies are equivalently costly in the worst case, we isolate query-dependent cost factors and present a method to choose between strategies, using new query cost estimation techniques. We evaluate our techniques using meaningful queries on biomedical data.
△ Less
Submitted 14 October, 2015;
originally announced October 2015.
