SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout

TL;DR

For the first time, Boolean variables are introduced to encode the hierarchy relationship among widgets and boost the reasoning ability of SMT solvers, boosting the reasoning ability of SMT solvers.

Abstract

Leveraging the flexible expressive ability of (Max)SMT and the powerful solving ability of SMT solvers, we propose a novel layout model named SMT-Layout. SMT-Layout is the first constraint-based layout model that can support real-time interaction for real-world GUI layout adapting to various screen sizes with only one specification. Previous works neglect the hierarchy information among widgets and thus cannot exploit the reasoning ability of solvers. For the first time, we introduce Boolean variables to encode the hierarchy relationship, boosting the reasoning ability of SMT solvers. The workflow is divided into two stages. At the development end, two novel preprocessing methods are proposed to simplify constraints and extract useful information in advance, easing the solving burden. After deploying constraints to the terminal end, SMT solvers are applied to solve constraints incrementally. Besides mainstream SMT solvers, a local search solver is customized to this scenario. Experiments show that SMT-Layout can support millisecond-level interaction for real-world layouts, even on devices with low computing power and rigorous memory limitations.

Figures (12)

• Figure 1: The two-stage workflow architecture of SMT-Layout.
• Figure 2: The numerical properties of widgets.
• Figure 3: Alternative layouts with varying screen size: The range of screen width is $[1000,2000]$. The wide version on the left is presented if the screen width is in the interval $[1500,2000]$. Otherwise, the compact version on the right is presented in the interval $[1000,1500)$.
• Figure 4: The corresponding hierarchical relationship. Blue item item denotes the Placeholder containers.
• Figure 5: Independent widgets Extraction: $Wide\_bar$ and $3\_col\_Table$ are independent widgets, since their $sub\_constraints$ do not affect widgets outside their sub-layouts, and can be extracted. In the solving module, (a) the overall layout in the outer layer is determined at the abstraction level, and (b) the sub-layouts in the inner layer are refined at the refinement level.

Theorems & Definitions (6)

• Example 1
• Example 2
• Example 3
• Example 4
• Example 5
• Example 6