Declarative GUI layout synthesis with relational constraint solvers

Authors describe a system which, given a set of designer-specified layout constraints (guidelines) and a description of graphic user interface (GUI) logical structure generates a set of particular layouts. Each of these layouts comply with given guidelines by construction. Authors also give a formal treatment of the task as a constraint satisfiability problem and describe the construction of a sound and complete solver based on the utilization of relational verifier-to-solver approach. They also describe a number of refinements which make the solver more efficient and applicable.