Chinese calligraphy is a quintessential element of Chinese cultural heritage. Analyzing and comparing calligraphic styles not only enhances the appreciation, learning, and advancement of calligraphy but also provides valuable insights into ancient China. However, such analysis remains challenging due to the limited scalability and possible inconsistencies of qualitative methods, as well as usability and misalignment issues in conventional quantitative approaches. We propose Calli-VA, a visual analytics system, to address these challenges. Calli-VA extracts character images and their corresponding strokes from original works and characterizes each character using systematic criteria. During analysis, the system defines the analysis scope by overview and uncovers relationships between characters. Explanation and recommendation mechanisms are integrated to help users understand patterns and guide further exploration. A documentation feature allows users to record and share their findings. We demonstrate the effectiveness of Calli-VA through three case studies and expert feedback.

The design of level shifters for high-voltage and high-speed applications must achieve low propagation delays while maintaining high immunity to power supply slew rates. A novel floating voltage level shifter with rapid operation, high power supply slew tolerance, and almost zero static power consumption is introduced. The conversion principle of the circuit is comprehensively analyzed. Additionally, a series of innovative optimization techniques are implemented to enhance switching speed and power supply slew tolerance, eliminate the asymmetry of rise and fall delays, and reduce power consumption and silicon area. The level shifter is designed using 0.18μm BCD technology, and post-layout simulations are performed by extracting parasitic parameters. The simulation results indicate that, at a level-shifting voltage of 45V, the proposed level-shifter achieves a propagation delay of 0.76ns, 300 V/ns ofdVSSH/dtslew rate immunity, and a single transition energy of 31.2pJ, with near-symmetrical rise and fall propagation delays.

In database-as-a-service platforms, automated ver-ification of query equivalence helps eliminate redundant computation in the form of overlapping sub-queries. Researchers have proposed two pragmatic techniques to tackle this problem. The first approach consists of reducing the queries to algebraic expressions and proving their equivalence using an algebraic theory. The limitations of this technique are threefold. It cannot prove the equivalence of queries with significant differences in the attributes of their relational operators (e.g., predicates in the filter operator). It does not support certain widely-used SQL features (e.g., NULL values). Its verification procedure is computationally intensive. The second approach transforms this problem to a constraint satisfaction problem and leverages a general-purpose solver to determine query equivalence. This technique consists of deriving the symbolic representation of the queries and proving their equivalence by determining the query containment relationship between the symbolic expressions. While the latter approach addresses all the limitations of the former technique, it only proves the equivalence of queries under set semantics (i.e., output tables must not contain duplicate tuples). However, in practice, database applications use bag semantics (i.e., output tables may contain duplicate tuples) In this paper, we introduce a novel symbolic approach for proving query equivalence under bag semantics. We transform the problem of proving query equivalence under bag semantics to that of proving the existence of a bijective, identity map between tuples returned by the queries on all valid inputs. We classify SQL queries into four categories, and propose a set of novel category-specific verification algorithms. We implement this symbolic approach in SPES and demonstrate that it proves the equivalence of a larger set of query pairs (95/232) under bag semantics compared to the SOTA tools based on algebraic (30/232) and symbolic approaches (67/232) under set and bag semantics, respectively. Furthermore, SPES is 3X faster than the symbolic tool that proves equivalence under set semantics.

Predicate-centric rules for rewriting queries is a key technique in optimizing queries. These include pushing down the predicate below the join and aggregation operators, or optimizing the order of evaluating predicates. However, many of these rules are only applicable when the predicate uses a certain set of columns. For example, to move the predicate below the join operator, the predicate must only use columns from one of the joined tables. By generating a predicate that satisfies these column constraints and preserves the semantics of the original query, the optimizer may leverage additional predicate-centric rules that were not applicable before. Researchers have proposed syntax-driven rewrite rules and machine learning algorithms for inferring such predicates. However, these techniques suffer from two limitations. First, they do not let the optimizer constrain the set of columns that may be used in the learned predicate. Second, machine learning algorithms do not guarantee that the learned predicate preserves semantics. In this paper, we present SIA, a system for learning predicates while being guided by counter-examples and a verification technique, that addresses these limitations. The key idea is to leverage satisfiability modulo theories to generate counter-examples and use them to iteratively learn a valid, optimal predicate. We formalize this problem by proving the key properties of synthesized predicates. We implement our approach in SIA and evaluate its efficacy and efficiency. We demonstrate that it synthesizes a larger set of valid predicates compared to prior approaches. On a collection of 200 queries derived from the TPC-H benchmark, SIA successfully rewrites 114 queries with learned predicates. 66 of these rewritten queries exhibit more than 2X speed up.