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

Bohan Li; Dawei Li; Ming Fu; Shaowei Cai

REVIEW 3 major objections 6 minor 42 references

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

T0 review · 3 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A single MaxSMT specification can drive real-time GUI layout across screen sizes on low-power devices.

desk verdict Interesting and mostly credible MaxSMT-based GUI layout system, but the one-specification guarantee rests on an unproven continuity assumption that the paper's own repair algorithm does not actually fix. read the letter →

arxiv 2411.12271 v1 pith:V7MCDUIF submitted 2024-11-19 cs.LO cs.HC

Bohan Li , Dawei Li , Ming Fu , Shaowei Cai This is my paper · ORCID

classification cs.LOcs.HC

keywords constraint-basedlayoutMaxSMTsolvingGUIscreenadaptationBooleanvisibilityencodinglocalsearchsolverpreprocessing

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes SMT-Layout, a constraint-based GUI layout model that aims to be the first to combine three properties: it handles real-world layouts, responds in real time, and adapts to many screen sizes from a single specification. The key move is to encode the visibility of each widget as a Boolean variable and to express hierarchy relationships with Boolean constraints, so an SMT solver's automated reasoning can discard constraints for invisible widgets. To make solving fast enough, heavy work is moved to a development stage: one preprocessor converts the MaxSMT formula into ordinary SMT formulas by detecting which soft alternatives fit which screen-width intervals, and another extracts independent sub-layouts that can be solved separately. At the terminal stage, the remaining formulas are solved incrementally by a complete solver or by a lightweight local-search solver. If the claim holds, designers would no longer maintain separate synchronized layouts for phone, tablet, and desktop widths.

What carries the argument

The load-bearing object is the Boolean visibility variable attached to every widget, denoted $[w]_v$, together with the automatically generated hard Boolean constraints that encode hierarchy. These constraints say, for example, that a visible widget has exactly one visible parent, that a visible ordinary container makes all its children visible, and that a visible Placeholder selects exactly one alternative child. This encoding lets the solver prune invisible subtrees before arithmetic solving. On top of it, the Interval-based soft constraints hardening preprocessor repeatedly calls MaxSMT and OMT solvers at development time to partition the screen-width range into intervals, each tied to one truth assignment of the soft constraints; those assignments are then baked in as unit clauses, converting MaxSMT to SMT. Independent widgets extraction splits off sub-formulas whose widgets do not interact with the rest, with intrinsic width and height bounds re-inserted into the outer formula. At the terminal end, a two-level abstraction/refinement solve uses either a complete SMT solver or a lightweight local-search solver customized with unit-equation elimination.

What would settle it

Construct a layout, for instance with a Placeholder whose wide alternative becomes feasible only for widths below 400 and above 800 while the compact alternative is feasible in between, and apply the hardening algorithm without the preview repair. Then solve the resulting SMT formula at a gap width such as 600: if the paper's central assumption holds, the formula is satisfiable and yields the expected layout; if the assumption fails, the formula is unsatisfiable or returns a layout inconsistent with the intended alternatives. Running this on one concrete counterexample would settle whether the preprocessing is sound as stated.

Watch

Extended reading notes

Core claim

The paper's central claim is that SMT-Layout is the first practical constraint-based layout model that can support real-time interaction for real-world GUI layouts adapting to various screen sizes with only one specification. Previous constraint-based models either require multiple synchronized specifications per screen size or, like OR-constraint layouts, cannot handle real-world widgets or respond within interactive time. The paper argues that the missing ingredient was Boolean structure: by introducing a visibility Boolean variable for each widget and hard Boolean constraints describing parent-child and alternative relationships, the hierarchy becomes visible to the SMT solver, which can then infer invisible widgets and drop their constraints. Two development-time preprocessing steps, the interval-based soft constraints hardening and independent widget extraction, turn the MaxSMT specification into smaller SMT formulas keyed to screen-width intervals; at terminal time, these are solved incrementally. Experiments on 12 real-world layouts report average interaction times below 25 ms on a phone, often below 1 ms with the local-search backend, and memory usage in the low megabytes.

Load-bearing premise

The method's speedup depends on the assumption used in Interval-based soft constraints hardening: for each fixed truth assignment of the soft constraints, the screen widths where that assignment is feasible form one continuous interval. If the feasible set is actually split into disjoint intervals, the generated correspondence constraint can be false at the gap widths, making the deployed SMT formula unsatisfiable or wrong unless the preview repair step catches and re-hardens the interval.

Editorial extensions

If this is right

Designers maintain a single layout specification instead of several synchronized variants for each target screen size.
Terminal devices with weak CPUs and tight memory can resize real-world pages at interactive rates, since most reasoning was moved to development time.
SMT solvers' Boolean reasoning shrinks the deployed formulas by dropping constraints of invisible widgets, which is where the largest reduction comes from.
The layout model is not tied to specific layout patterns, so new container types can be added without designing new solver heuristics.
For incremental resizing, a local-search backend is substantially faster and uses far less memory than a complete solver, because most constraints stay satisfied between consecutive widths.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the interval-continuity assumption fails in practice more often than the authors expect, the preview repair step becomes load-bearing rather than a safety net; a robust extension would encode discontiguous feasible sets directly into the relation instead of patching them after the fact.
The same interval-hardening scheme could be applied to other continuous parameters, such as window height, aspect ratio, or font size, possibly yielding responsive layouts that adapt along more than one axis without multiplying specifications.
Because the local-search backend is an incomplete solver, its millisecond numbers may not transfer to pathological layouts where many constraints change at once; a hybrid policy that switches to the complete solver when few constraints remain satisfied would be a natural test.
The main practical bottleneck the paper leaves open is authoring: without a visual editor or reverse engineering of existing pages, designers must hand-write the API specifications, which is time-consuming and may limit adoption.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's my take: this paper is worth engaging. The new modeling idea—Boolean visibility variables that encode widget hierarchy—is a real step beyond ORCLayout, and the engineering results are genuinely good: 12 real-world-style layouts, single specification across widths, millisecond interaction on a phone, with ablations showing the preprocessing and the LocalSMT backend each contribute large speedups. If I were building a responsive layout tool, I'd want to read this.

The soft spots are real, though. The formal typos in Eqs. 2 and 5 ([w]p where it should be [w]v) are easy to fix but make the core encoding hard to follow. More importantly, the interval-based hardening step is load-bearing and only as sound as the assumption that each soft constraint assignment is feasible on one continuous width interval. Section 6 explicitly admits this can fail, and the preview repair in Appendix B does not repair it: Algorithm 3 line 9 tries to read a soft assignment from a formula that is unsatisfiable, and even if one supplies that assignment from the original MaxSMT, reapplying hardening can produce two contradictory equivalences for the same assignment. The result is an SMT formula that is not equivalent to the MaxSMT specification at gap widths. Since the central 'one specification, every width' claim depends on this conversion, the paper needs a proof of continuity for its benchmark class, or a fallback that provably restores equivalence. Acknowledging the limitation is honest, but it remains a correctness gap in the main contribution.

Lesser issues: the comparison to ORCSolver is declared missing, with reasons given, but the crash claim is not independently verifiable from the paper; the benchmarks are all self-specified; and the LocalSMT backend is the authors' own prior solver, which is fine, but the incremental benefit of the customization is hard to separate from the solver's baseline strength.

Bottom line: this is a serious paper with a significant idea and convincing engineering. The gap is real but addressable—a proof or bounded check of the continuity property, plus a repair step that provably terminates with an equivalent formula. I'd send it to review, with major revision requested on precisely that point. I would cite it if my work touched layout constraints, and I'd bring it to a reading group as a good case study in preprocessing correctness for MaxSMT.

Referee Report

3 major / 6 minor

Summary. The paper proposes SMT-Layout, a constraint-based GUI layout model based on MaxSMT. It introduces Boolean visibility variables for widgets to specify hierarchical relationships, a Placeholder container for alternative layouts, and a two-stage workflow: preprocessing at development time (interval-based soft-constraint hardening and independent-widget extraction) and incremental solving at the terminal end using Z3 or a customized local-search solver LocalSMT. The paper claims this is the first approach supporting real-time interaction for real-world layouts adapting to various screen sizes with a single specification. Experiments on 12 benchmarks derived from real-world web and mobile GUIs report millisecond-level interaction times and low memory usage with LocalSMT.

Significance. If the preprocessing were sound and the conversion from MaxSMT to SMT equivalence-preserving, the paper would be a significant contribution: the Boolean encoding of hierarchy is a sensible idea to leverage SMT reasoning, the two-stage workflow is practical, and the evaluation is substantial (12 real-world benchmarks, two devices, ablations, anonymous repo). The 93.6%/91.6% average/maximum time reductions from hardening and the 56.5%/53.2% reductions from independent-widget extraction (Table 4) suggest the techniques are effective in the tested settings. However, the central soundness issue described below prevents acceptance in the current form.

major comments (3)

[§5.1 (Algorithm 1) and §6 (Appendix B)] The Interval-based soft constraints hardening is unsound when the feasible set of a soft assignment α_soft is disconnected. In Algorithm 1, line 7 computes the global minimum of p over Fmax.hard ∧ (∧_{ℓ∈α_soft} ℓ); for a set such as [1000,1400]∪[1600,2000] this yields (α ←→ 1000≤p≤2000) at line 8, which is false at p=1500, making the deployed SMT formula unsatisfiable exactly at that width. Section 6 acknowledges the discontinuity, but Algorithm 3 cannot repair it: after F∧(p==curr_p) is unsat, line 9 requires 'the assignment of soft constraints,' yet an unsatisfiable formula has no model, and the model of Fmax.hard∧(p==curr_p) from line 5 does not determine the soft Boolean variables. Moreover, re-hardening with (α_soft → p > curr_p) and replacing F discards the previously found interval [1000,1400], so the new formula no longer encodes the original preference at those widths. No termination or equivalence proof for the preview loop is provided. Because this preprocessing is the load-bearing step that converts the MaxSMT specification into the SMT formula deployed at the terminal end, the central claim that a single specification produces correct real-time layouts at every screen width is not established for the general case.
[§4.4 and §5.1] The hardening precondition 'soft constraints related to p' covers only the Placeholder-visibility soft constraints of Eq. (8). However, Section 4.4 also introduces type-1 soft constraints: auxiliary Boolean variables soft_new with hard constraint soft_new → F_conj (Eq. 7). These variables are not determined by the screen width p, so substituting C_relation for the soft constraints leaves them as unconstrained Boolean variables in the converted SMT formula, and their weights no longer influence the solution. The paper should either restrict the modeling language to placeholder-only soft constraints or provide an additional mechanism (e.g., treating type-1 soft constraints as hard requirements or as lexicographic objectives) that preserves their semantics after the MaxSMT-to-SMT conversion. As written, the one-specification claim does not cover the full modeling API presented in Section 4.4.
[§4.3, Eqs. (2) and (5)] Equations (2) and (5) use [w]p as the antecedent of the implication. But [w]p was defined as the set of parent containers, not a Boolean formula; the intended antecedent is the visibility property [w]v, consistent with Eqs. (1), (3), (4), and (6). As printed, these are not well-formed formulas and cannot be fed to an SMT solver. This is a formal error in the core hierarchy constraints and should be corrected.

minor comments (6)

[Table 3 and Table 4] The header 'benchamrk' in Table 3 and the extra parenthesis in the 'Bilibili app' row of Table 4 ('0.95 (10.1) ) 3.9') are typos that should be fixed.
[§2.1 and Algorithm 3] The domain of the size property p is not stated; Algorithm 3's step curr_p := curr_p − 1 assumes a discrete integer domain with unit step, but the background theory is linear arithmetic over the reals. If p is real-valued, the preview traversal does not terminate.
[§5.2] The threshold t = 300 for independent widgets is an arbitrary parameter; a brief sensitivity analysis would strengthen the claim that the method does not hinge on this choice.
[§4.1] The notation [w]w for the width of widget w is confusing because the same symbol denotes the widget; consider renaming the width property (e.g., w.width) to avoid collision.
[§8] The statement that the maximum interaction time occurs when entering a new interval is plausible but not backed by per-event statistics; a short table or figure would be useful.
[§10] The 'first' claim should be qualified (e.g., 'to the best of our knowledge') and scoped to the combination of MaxSMT with Boolean hierarchy variables, since the related-work survey is not exhaustive.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the preprocessing converts a MaxSMT specification into an SMT formula by logical construction, not by fitting or by importing a uniqueness result from prior work.

full rationale

SMT-Layout makes no empirical prediction that is fitted to data and then re-reported; the Interval-based soft constraints hardening (Algorithm 1) builds C_relation by solving the same MaxSMT formula and recording, for each soft assignment, the feasible interval of the size property. That is a rewrite of the input specification rather than a circular derivation, and the paper does not rename a fitted parameter as a prediction. The self-citations to LocalSMT [20-22] are normal tool attribution: LocalSMT is evaluated as a backend solver against Z3, the benchmarks are deposited in an anonymous repository, and the Z3-based version independently supports the millisecond-level claim, so the self-citation is not load-bearing. Section 6 does state a real limitation: "This is based on the assumption that the interval is continuous… however, although the probability is low, the feasible interval corresponding to αso f t values may be discontinuous." This is a soundness gap for the preprocessing (and Algorithm 3's repair is not fully specified), but it is a correctness risk, not a circularity pattern: C_relation is not defined in terms of its own output, no equation is equivalent to its input by construction, and no uniqueness theorem from the authors is invoked to force a choice. The central "one specification" claim therefore stands or falls on the empirical evaluation and on the missing continuity proof, not on circular reasoning.

Assumptions & free parameters 1 free parameters · 6 assumptions · 2 invented entities

The central pipeline rests on four domain assumptions (vertical scrolling, interval continuity, local-search-friendly incremental changes, modular independence) and one hand-chosen threshold. The continuity assumption is explicitly acknowledged as fallible in Section 6, and the others are plausible but not independently validated.

free parameters (1)

Independent widget clause threshold t = 300
Chosen by hand in Section 5.2 to limit the size of extracted sub-constraints; no sensitivity analysis is given.

assumptions (6)

domain assumption For typical layouts, screen height has minimal impact because pages scroll vertically, so only screen width is modeled.
Section 3 states this to justify focusing on width; if false for desktop or TV layouts without scrolling, the single-specification claim weakens.
ad hoc to paper The set of screen widths for which a given soft-constraint assignment is feasible is a continuous interval.
Section 6 explicitly assumes continuity in Algorithm 1; the preview module patches discontinuities, but the core preprocessing as written is unsound without it.
domain assumption Most constraints remain satisfied as screen width varies, so local search near the current solution is efficient.
Section 7.2 motivates LocalSMT; empirically supported only by average iteration 15.6 on self-authored benchmarks.
domain assumption Widgets can be partitioned into independent sub-layouts whose constraints do not affect outside widgets.
Section 5.2 defines independence and relies on modular design practice; the restriction to widgets with irrelevant width and height is unvalidated.
domain assumption Sub-layouts can be translated, so positional properties x and y can be set to 0 in extracted constraints.
Section 5.2 uses translation invariance to drop positional constraints; this holds for absolute coordinates but not for constraints tying the sub-layout to external widgets.
standard math Linear arithmetic SMT and OMT solvers (Z3, nuZ) correctly decide satisfiability and optimize objectives for the generated formulas.
Used throughout preprocessing and solving; the paper does not prove solver correctness and relies on Z3 and prior OMT methods.

invented entities (2)

Boolean visibility property [w]v per widget
purpose: Encodes whether a widget is displayed; used to formalize hierarchy and enable SMT Boolean reasoning.
A modeling construct with no falsifiable handle outside the paper; its value is validated only by solver performance, not by external prediction.
Placeholder container
purpose: Groups alternative widgets that switch by screen width, enabling a single specification to cover multiple layouts.
A new layout container type in the modeling API; it is an engineering abstraction, not an empirically testable entity.

how reviews work

0 comments

Cite this review

Pith. "Pith review of SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout." pith.science (2026). https://pith.science/paper/V7MCDUIF

@misc{pith2026241112271,
  author       = {Pith},
  title        = {Pith review of: SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/V7MCDUIF}},
  note         = {Machine review of arXiv:2411.12271}
}

read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 41 canonical work pages

[1]

In: 19th Australian Conference on Software Engineering (aswec 2008), pp

Lutteroth, C., Weber, G.: Modular specification of gui layout using constraints. In: 19th Australian Conference on Software Engineering (aswec 2008), pp. 300–309 (2008). IEEE

work page 2008
[2]

In: Proceedings of the 7th Australasian User Interface conference-Volume 50, pp

Lutteroth, C., Weber, G.: User interface layout with ordinal and linear con- straints. In: Proceedings of the 7th Australasian User Interface conference-Volume 50, pp. 53–60 (2006)

work page 2006
[3]

In: Proceedings of the 24th Australian Computer-Human Interaction Conference, pp

Zeidler, C., M¨ uller, J., Lutteroth, C., Weber, G.: Comparing the usability of grid-bag and constraint-based layouts. In: Proceedings of the 24th Australian Computer-Human Interaction Conference, pp. 674–682 (2012)

work page 2012
[4]

Addison-Wesley Professional, ??? (2013)

Sadun, E.: iOS Auto Layout Demystified. Addison-Wesley Professional, ??? (2013)

work page 2013
[5]

” O’Reilly Media, Inc.”, ??? (2017)

Weyl, E.: Flexbox in CSS. ” O’Reilly Media, Inc.”, ??? (2017)

work page 2017
[6]

ACM Transactions on Computer-Human Interaction (TOCHI) 8(4), 267–306 (2001)

Badros, G.J., Borning, A., Stuckey, P.J.: The cassowary linear arithmetic con- straint solving algorithm. ACM Transactions on Computer-Human Interaction (TOCHI) 8(4), 267–306 (2001)

work page 2001
[7]

Technical report, University of Washington (1992)

Bill, T., Lundell, B., McDonald, J.A., Sannella, M.: Bricklayer: window layout using linear programming. Technical report, University of Washington (1992)

work page 1992
[8]

In: Proceedings of the 10th Annual ACM Symposium on User Interface Software and Technology, pp

Borning, A., Marriott, K., Stuckey, P., Xiao, Y.: Solving linear arithmetic con- straints for user interface applications. In: Proceedings of the 10th Annual ACM Symposium on User Interface Software and Technology, pp. 87–96 (1997)

work page 1997

Show all 42 references

[9]

In: International Conference on Principles and Practice of Constraint Programming, pp

Hosobe, H.: A scalable linear constraint solver for user interface construction. In: International Conference on Principles and Practice of Constraint Programming, pp. 218–233 (2000). Springer

2000
[10]

Constraints 13, 307–342 (2008)

Lutteroth, C., Strandh, R., Weber, G.: Domain specific high-level constraints for user interface layout. Constraints 13, 307–342 (2008)

2008
[11]

In: Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems, pp

Jiang, Y., Du, R., Lutteroth, C., Stuerzlinger, W.: Orc layout: Adaptive gui lay- out with or-constraints. In: Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems, pp. 1–12 (2019)

2019
[12]

In: Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems, pp

Jiang, Y., Stuerzlinger, W., Zwicker, M., Lutteroth, C.: Orcsolver: An efficient solver for adaptive gui layout with or-constraints. In: Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems, pp. 1–14 (2020)

2020
[13]

In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp

Moura, L.d., Bjørner, N.: Z3: An efficient smt solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337– 340 (2008). Springer 36

2008
[14]

Springer, ??? (2016)

Kroening, D., Strichman, O.: Decision Procedures. Springer, ??? (2016)

2016
[15]

In: Computer Aided Verification: 16th International Conference, CA V 2004, Boston, MA, USA, July 13-17, 2004

Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Dpll (t): Fast decision procedures. In: Computer Aided Verification: 16th International Conference, CA V 2004, Boston, MA, USA, July 13-17, 2004. Proceedings 16, pp. 175–188 (2004). Springer

2004
[16]

Biere, A., Heule, M., Maaren, H.: Handbook of Satisfiability vol. 185. IOS press, ??? (2009)

2009
[17]

In: Proceedings of the AAAI Conference on Artificial Intelligence, vol

Fr¨ ohlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 29 (2015)

2015
[18]

In: International Conference on Computer Aided Verification, pp

Niemetz, A., Preiner, M., Biere, A.: Precise and complete propagation based local search for satisfiability modulo theories. In: International Conference on Computer Aided Verification, pp. 199–217 (2016). Springer

2016
[19]

Formal Methods in System Design 51(3), 608–636 (2017)

Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods in System Design 51(3), 608–636 (2017)

2017
[20]

ACM Transactions on Computational Logic 24(4), 1–26 (2023)

Cai, S., Li, B., Zhang, X.: Local search for satisfiability modulo integer arithmetic theories. ACM Transactions on Computational Logic 24(4), 1–26 (2023)

2023
[21]

In: International Conference on Computer Aided Verification, pp

Cai, S., Li, B., Zhang, X.: Local search for smt on linear integer arithmetic. In: International Conference on Computer Aided Verification, pp. 227–248 (2022). Springer

2022
[22]

In: CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN– FMCAD 2023, p

Li, B., Cai, S.: Local search for smt on linear and multi-linear real arithmetic. In: CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN– FMCAD 2023, p. 168 (2023)

2023
[23]

In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, pp

Zakai, A.: Emscripten: an llvm-to-javascript compiler. In: Proceedings of the ACM International Conference Companion on Object Oriented Programming Systems Languages and Applications Companion, pp. 301–312 (2011)

2011
[24]

Bjørner, N., Phan, A.-D., Fleckenstein, L.: νz-an optimizing smt solver. In: Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2...

2015
[25]

ACM Transactions on Computer-Human Interaction (TOCHI) 7(1), 3–28 (2000) 37

Myers, B., Hudson, S.E., Pausch, R.: Past, present, and future of user interface software tools. ACM Transactions on Computer-Human Interaction (TOCHI) 7(1), 3–28 (2000) 37

2000
[26]

ACM Transactions on Computer- Human Interaction (TOCHI) 2(1), 64–103 (1995)

Myers, B.A.: User interface software tools. ACM Transactions on Computer- Human Interaction (TOCHI) 2(1), 64–103 (1995)

1995
[27]

In: 2010 21st Australian Software Engineering Conference, pp

Weber, G.: A reduction of grid-bag layout to auckland layout. In: 2010 21st Australian Software Engineering Conference, pp. 67–74 (2010). IEEE

2010
[28]

Journal of Logical and Algebraic Methods in Programming 89, 67–94 (2017)

Zeidler, C., Weber, G., Gavryushkin, A., Lutteroth, C.: Tiling algebra for constraint-based layout editing. Journal of Logical and Algebraic Methods in Programming 89, 67–94 (2017)

2017
[29]

Eduvantage 1(1) (2013)

Natda, K.V.: Responsive web design. Eduvantage 1(1) (2013)

2013
[30]

In: 2013 36th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), pp

Mohoroviˇ ci´ c, S.: Implementing responsive web design for enhanced web pres- ence. In: 2013 36th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), pp. 1206–1210 (2013). IEEE

2013
[31]

Procedia-Social and Behavioral Sciences 106, 2275–2279 (2013)

Baturay, M.H., Birtane, M.: Responsive web design: a new type of design for web-based instructional content. Procedia-Social and Behavioral Sciences 106, 2275–2279 (2013)

2013
[32]

In: Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, pp

Sahami Shirazi, A., Henze, N., Schmidt, A., Goldberg, R., Schmidt, B., Schmauder, H.: Insights into layout patterns of mobile user interfaces by an automatic analysis of android apps. In: Proceedings of the 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems,...

2013
[33]

In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, pp

Zanden, B.V., Myers, B.A.: Automatic, look-and-feel independent dialog creation for graphical user interfaces. In: Proceedings of the SIGCHI Conference on Human Factors in Computing Systems, pp. 27–34 (1990)

1990
[34]

ACM Transactions on Programming Languages and Systems (TOPLAS) 14(3), 339–395 (1992)

Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.: The clp (r) language and sys- tem. ACM Transactions on Programming Languages and Systems (TOPLAS) 14(3), 339–395 (1992)

1992
[35]

Communications of the ACM 33(1), 54–63 (1990)

Freeman-Benson, B.N., Maloney, J., Borning, A.: An incremental constraint solver. Communications of the ACM 33(1), 54–63 (1990)

1990
[36]

Software: Practice and Experience 23(5), 529–566 (1993)

Sannella, M., Maloney, J., Freeman-Benson, B., Borning, A.: Multi-way versus one-way constraints in user interfaces: Experience with the deltablue algorithm. Software: Practice and Experience 23(5), 529–566 (1993)

1993
[37]

In: Proceedings of the 7th Annual ACM Symposium on User Interface Software and Technology, pp

Sannella, M.: Skyblue: A multi-way local propagation constraint solver for user interface construction. In: Proceedings of the 7th Annual ACM Symposium on User Interface Software and Technology, pp. 137–146 (1994)

1994
[38]

In: International Conference on Principles 38 and Practice of Constraint Programming, pp

Marriott, K., Chok, S.S., Finlay, A.: A tableau based constraint solving toolkit for interactive graphical applications. In: International Conference on Principles 38 and Practice of Constraint Programming, pp. 340–354 (1998). Springer

1998
[39]

Constraints 7, 229–254 (2002)

Marriott, K., Sen Chok, S.: Qoca: A constraint solving toolkit for interactive graphical applications. Constraints 7, 229–254 (2002)

2002
[40]

In: 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence, pp

Hosobe, H.: A simplex-based scalable linear constraint solver for user interface applications. In: 2011 IEEE 23rd International Conference on Tools with Artificial Intelligence, pp. 793–798 (2011). IEEE

2011
[41]

In: Walsh, T

Marriott, K., Moulder, P., Stuckey, P.J., Borning, A.: Solving disjunctive con- straints for interactive graphical applications. In: Walsh, T. (ed.) Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 ...

2001 doi
[42]

In: Proceedings of the 13th International Conference of the NZ Chapter of the ACM’s Special Interest Group on Human-Computer Interaction, pp

Zeidler, C., Lutteroth, C., Weber, G.: Constraint solving for beautiful user inter- faces: how solving strategies support layout aesthetics. In: Proceedings of the 13th International Conference of the NZ Chapter of the ACM’s Special Interest Group on Human-Computer Interaction...

2012

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [1]

In: 19th Australian Conference on Software Engineering (aswec 2008), pp

Lutteroth, C., Weber, G.: Modular specification of gui layout using constraints. In: 19th Australian Conference on Software Engineering (aswec 2008), pp. 300–309 (2008). IEEE

work page 2008

[2] [2]

In: Proceedings of the 7th Australasian User Interface conference-Volume 50, pp

Lutteroth, C., Weber, G.: User interface layout with ordinal and linear con- straints. In: Proceedings of the 7th Australasian User Interface conference-Volume 50, pp. 53–60 (2006)

work page 2006

[3] [3]

In: Proceedings of the 24th Australian Computer-Human Interaction Conference, pp

Zeidler, C., M¨ uller, J., Lutteroth, C., Weber, G.: Comparing the usability of grid-bag and constraint-based layouts. In: Proceedings of the 24th Australian Computer-Human Interaction Conference, pp. 674–682 (2012)

work page 2012

[4] [4]

Addison-Wesley Professional, ??? (2013)

Sadun, E.: iOS Auto Layout Demystified. Addison-Wesley Professional, ??? (2013)

work page 2013

[5] [5]

” O’Reilly Media, Inc.”, ??? (2017)

Weyl, E.: Flexbox in CSS. ” O’Reilly Media, Inc.”, ??? (2017)

work page 2017

[6] [6]

ACM Transactions on Computer-Human Interaction (TOCHI) 8(4), 267–306 (2001)

Badros, G.J., Borning, A., Stuckey, P.J.: The cassowary linear arithmetic con- straint solving algorithm. ACM Transactions on Computer-Human Interaction (TOCHI) 8(4), 267–306 (2001)

work page 2001

[7] [7]

Technical report, University of Washington (1992)

Bill, T., Lundell, B., McDonald, J.A., Sannella, M.: Bricklayer: window layout using linear programming. Technical report, University of Washington (1992)

work page 1992

[8] [8]

In: Proceedings of the 10th Annual ACM Symposium on User Interface Software and Technology, pp

Borning, A., Marriott, K., Stuckey, P., Xiao, Y.: Solving linear arithmetic con- straints for user interface applications. In: Proceedings of the 10th Annual ACM Symposium on User Interface Software and Technology, pp. 87–96 (1997)

work page 1997