Ali Abbassi

Jui-Ting Lu, Henrique Ennes, Chih-Kang Huang et al.

Quantum brushes are computational arts software introduced by Ferreira et al (2025) that leverage quantum behavior to generate novel artistic effects. In this outreach paper, we introduce the mathematical framework and describe the implementation of two quantum brushes based on variational quantum algorithms, Steerable and Chemical. While Steerable uses quantum geometric control theory to merge two works of art, Chemical mimics variational eigensolvers for estimating molecular ground energies to evolve colors on an underlying canvas. The implementation of both brushes is available open-source at https://github.com/moth-quantum/QuantumBrush and is fully compatible with the original quantum brushes.

Ali Abbassi, Nancy A. Day, Derek Rayside

We present a variety of translation options for converting Alloy to SMT-LIB via Alloy's Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational operations of Alloy into their equivalent in typed first-order logic (TFOL). We investigate and compare the performance of an SMT solver for many translation options. We compare using only one universal type to recovering Alloy type information from the Kodkod representation and using multiple types in TFOL. We compare a direct translation of the relations to predicates in TFOL to one where we recover functions from their relational form in Kodkod and represent these as functions in TFOL. We compare representations in TFOL with unbounded scopes to ones with bounded scopes, either pre or post quantifier expansion. Our results across all these dimensions provide directions for portfolio solvers, modelling improvements, and optimizing SMT solvers.