University of California, Santa Cruz, Baskin School of Engineering
Originally a hardware engineer, I received my bachelor's and first master's degrees in computer engineering from Drexel University in Philadelphia, PA. I spent over 10 years working in industry primarily on wireless power semiconductors for consumer cellular and wearable electronics.
As my career progressed, I chose to transition to the rapidly evolving machine learning and artificial intelligence (AI) domains. I received my second master's degree in computer science from San José State University in 2016. I am now a Ph.D. student at the University of California, Santa Cruz. The primary focus of my research is around problems in satisfiability. My current efforts specifically deal with efficient, uniformly random sampling from the set of satisfying assignments.
Advisor: Prof. Dimitris Achlioptas
University of California, Santa Cruz, Baskin School of Engineering
Integrated Device Technology Inc.
Drexel University, College of Engineering
University of California, Santa Cruz
San José State University
Computer Engineering (Dual Degree)
Today, machine learning trivially solves problems that only a few years ago were completely intractable. My research focus on applying machine learning techniques to different problems including satisfyability (SAT) problems.
The list below includes highlights of current and past research work on which I worked. If you have any questions or wish to collaborate, please do not hesitate to reach out to me directly.
Given a Boolean formula, F, the problem is to select s satisfying assignments uniformly, independently, with replacement (u.i.r.). This problem comes up in both software and hardware validation, in particular in Constrained Random Verification (CRV).
In this research, we modified the exact model counter sharpSAT to perform uniform SAT sampling. Our implementation, SPUR, guarantees uniformity through the use of reservoir sampling, which ensures SPUR is low overhead. The rule of thumb for our execution time is: "In 10x the time it takes sharpSAT to count the satisfying assignments, SPUR can generate 1,000 samples."
Source Code: Available on GitHub
While generally considered a leisure or children's activity, jigsaw puzzle solving is actually NP-complete when inter-piece similarity is not a reliable metric for determining piece adjaceny. The jig swap puzzle is a more challenging variant of the traditional jigsaw puzzle, wherein all pieces are equal-sized squares that must be placed adjacent to one another to reconstruct an original, unknown image.
In this research, we looked at techniques to reassemble jig swap puzzles without any external "oracle" information. We developed a clustering-based solver that outperforms the state-of-the-art in terms of the number of supportable inputs as well as the quality of the reconstructed outputs.
The following is a list of selected, refereed publications. Clicking on the publication will reveal the associated abstract. Clicking the "" button below any publication opens a link to download that specific document.
The jig swap puzzle is a variant of the traditional jigsaw puzzle, wherein all pieces are equal-sized squares that must be placed adjacent to one another to reconstruct an original, unknown image. This paper proposes an agglomerative hierarchical clustering-based solver that can simultaneously reconstruct multiple, mixed jig swap puzzles. Our solver requires no additional information beyond an unordered input bag of puzzle pieces, and it significantly outperforms the current state of the art in terms of both the reconstructed output quality as well the number of input puzzles it supports. In addition, we define the first quality metrics specifically tailored for multi-puzzle solvers, the Enhanced Direct Accuracy Score (EDAS), the Shiftable Enhanced Direct Accuracy Score (SEDAS), and the Enhanced Neighbor Accuracy Score (ENAS).
We present an algorithm for perfectly uniform sampling of satisfying assignments, based on the exact model counter sharpSAT and reservoir sampling. In experiments across several hundred formulas, our sampler is faster than the state of the art by 10 to over 100,000 times
We present a probabilistic model counter that can trade off running time with approximation accuracy. As in several previous works, the number of models of a formula is estimated by adding random parity constraints (equations). One key difference with prior works is that the systems of parity equations used correspond to the parity check matrices of Low Density Parity Check (LDPC) error-correcting codes. As a result, the equations tend to be much shorter, often containing fewer than 10 variables each, making the search for models that also satisfy the parity constraints far more tractable. The price paid for computational tractability is that the statistical properties of the basic estimator are not as good as when longer constraints are used. We show how one can deal with this issue and derive rigorous approximation guarantees by performing more solver invocations.
The square jigsaw puzzle is a variant of traditional jigsaw puzzles, wherein all pieces are equal-sized squares; these pieces must be placed adjacent to one another to reconstruct an original image. This thesis proposes an agglomerative hierarchical clustering based solver that can simultaneously reconstruct multiple square jigsaw puzzles. This solver requires no additional information beyond an input bag of puzzle pieces and significantly outperforms the current state of the art in terms of both the quality of the reconstructed outputs as well the number of input puzzles it supports. In addition, this thesis defines Enhanced Direct Accuracy Score (EDAS), Shiftable Enhanced Direct Accuracy Score (SEDAS), and Enhanced Neighbor Accuracy Score (ENAS), which are the first quality metrics specifically tailored for multi-puzzle solvers. This thesis also outlines the first standards for visualizing best buddies and the quality of solver solutions.
We describe ForPowER, a power-efficient architecture for handling fork-join parallelism using system on a chip. Our design consists of 16 processor cores, capable of dynamically scaling their clock frequencies and supply voltages under different workloads. The processors are divided into four sets of four, with each set sharing a multiported two-level cache. This arrangement reduces the energy wasted on powering redundant data. ForPowER also uses a central scheduler, which assigns tasks to the processors, taking advantage of the shared memory and of the processors ability to scale their clock frequencies under varied workload.
We also describe power models for all components of the SoC design, namely the caches, processors, and the network.
We show that in simulation, ForPowER outperforms the most widely used fork-join architecture on the SPEC-95 Hydro2D benchmark, saving over 65% more energy.
Below is a selection of current and previous courses I have taught at UC Santa Cruz and Drexel University.
Differential Equations, Transforms, and Fundamentals of Systems
Evaluation and Presentation of Experimental Data and Ethics
Here are some fun and interesting tidbits about me that you may or may not find interesting:
I am always looking for opportunities to collaborate with other researchers; I am also happy to answer any questions regarding my current or previous work. The best way to reach me is through my UCSC university email. This can also optionally be used to connect with me on Google Hangouts, but in most cases, my response time is good enough that an instant message is unnecessary.
Generally, I try to open-source all of my coursework notes and development material, which I publish through Github. If you observe bugs or errors in any of my repositories, I would sincerely appreciate if you contacted me directly or even better initiated a Github pull request.
My office is in the Engineering 2 building, room 489. The lab requires card access so please knock to get our attention.
I do not keep regular office hours although I am usually on campus every weekday and some weekends. Please contact me directly to schedule an appointment if you would like to meet.