Search for: All records

Constraints solvers play a significant role in the analysis, synthesis, and formal verification of complex cyber-physical systems. In this article, we study the problem of designing a scalable constraints solver for an important class of constraints named polynomial constraint inequalities (also known as nonlinear real arithmetic theory). In this article, we introduce a solver named PolyARBerNN that uses convex polynomials as abstractions for highly nonlinears polynomials. Such abstractions were previously shown to be powerful to prune the search space and restrict the usage of sound and complete solvers to small search spaces. Compared with the previous efforts on using convex abstractions, PolyARBerNN provides three main contributions namely (i) a neural network guided abstraction refinement procedure that helps selecting the right abstraction out of a set of pre-defined abstractions, (ii) a Bernstein polynomial-based search space pruning mechanism that can be used to compute tight estimates of the polynomial maximum and minimum values which can be used as an additional abstraction of the polynomials, and (iii) an optimizer that transforms polynomial objective functions into polynomial constraints (on the gradient of the objective function) whose solutions are guaranteed to be close to the global optima. These enhancements together allowed the PolyARBerNN solver to solve complex instances and scales more favorably compared to the state-of-the-art nonlinear real arithmetic solvers while maintaining the soundness and completeness of the resulting solver. In particular, our test benches show that PolyARBerNN achieved 100X speedup compared with Z3 8.9, Yices 2.6, and PVS (a solver that uses Bernstein expansion to solve multivariate polynomial constraints) on a variety of standard test benches. Finally, we implemented an optimizer called PolyAROpt that uses PolyARBerNN to solve constrained polynomial optimization problems. Numerical results show that PolyAROpt is able to solve high-dimensional and high order polynomial optimization problems with higher speed compared to the built-in optimizer in the Z3 8.9 solver. 

To cut CO₂emissions, we propose to directly convert shale gas into value-added products with a new H₂/O₂co-transport membrane (HOTM) reactor. A Multiphysics model has been built to simulate the membrane and the catalytic bed with parameters obtained from experimental validation. The model was used to compare C2 yield and CH₄conversion rate between the membrane reactor and the state-of-the-art fixed-bed reactor with the same dimensions and operating conditions. The results indicate that (1) the membrane reactor is more efficient in consuming CH₄for a given amount of fed O₂. (2) The C2 selectivity of the membrane reactor is higher due to the gradual addition of O₂into the reactor. (3) The current proposed membrane reactor can have a decent proton molar flux density but most of the proton molar flux will contribute to producing H₂O on the feed side under the current operating conditions. The paper for the first-time projects the performance of the membrane reactor for combined H₂O/H₂removal and C2 production. It could be used as important guidance for experimentalists to design next generation natural gas conversion reactors.

 

In this study, we simulated BZY electrolyte-supported proton-conducting solid oxide cell by coupling surface defect chemistry reaction with charged species transport. We validated the model parameters by concentration as a function of temperature, conductivity under dry and wet oxygen as a function of oxygen partial pressure and temperature. The results indicate that the high electron-hole mobility (diffusivity) is mainly responsible for the high leaking current under high temperatures. The Faradaic efficiency stays low or even negative under low operating voltage or high temperature and plateaus as the cell voltage increases. The model developed in this study is a useful tool to understand the leaking current in BZY electrolyte and provide design strategies to avoid/mitigate such significant inefficiency for water electrolysis operation.