Abstract

Abstract
This paper solves the resource-constrained project scheduling problem (RCPSP) with a satisfiability problem (SAT) solver. This paper builds further on various existing SAT models for this well-known project scheduling problem and extends them with two methods to satisfy the resource constraints. Specifically, we use the wellknown minimal forbidden sets and compare them with the so-called covers that are traditionally used in SAT implementations. Moreover, we also implement an existing binary decision trees approach under various settings and extend the model with networks with adders, so far never used for solving the RCPSP, to guarantee that resource constraints are satisfied. The algorithms are tested under different settings on a set of 13,413 project instances with diverse network and resource structures, and the experiments demonstrate that a combination of these approaches help in finding better solutions within a reasonable time. Moreover, 393 new lower bounds, 62 new upper bounds, and 290 optimally solved instances (including 18 from the PSPLIB) have been discovered, which, to the best of our knowledge, had not been found before. The strong performance of the new algorithm motivated additional experiments, and the preliminary results suggest several promising directions for future research.

Abstract
-This study focuses on providing meaningful information to vulnerable road users (VRUs) to support their objectives and perceptions while navigating urban spaces, employing a novel route planning concept. Through three focus group sessions, a comprehensive survey was conducted to identify the needs and concerns of VRUs, leading to the development of an integrated and collaborative mobile application for active mobility. The application encompasses route calculation, prioritizing safety, comfort, civic participation, and empathy. The solution aims to bridge citizen users and city managers, facilitating alerts, historical information on safety and comfort, and collaborative problem-solving and sharing of urban attractions. A prototype of the concept was developed and extensively tested by potential users, and subjective evaluation and feedback demonstrated the usefulness and added value of the integrated and collaborative approach. This study highlights the proposed solution relevance and differentiation from official alerts, user experiences, and civic participation, positioning it as a comprehensive solution for active mobility.

Abstract
The growing integration of Artificial Intelligence (AI) into interactive systems presents unique challenges and opportunities for Human-Computer Interaction (HCI) and User Experience (UX). While AI can enhance usability and provide novel interaction paradigms, it also raises concerns related to transparency, control, and user trust. This workshop seeks to bring together researchers and practitioners to discuss state-of-the-art engineering methods that support HCI and UX in AI-driven systems. By fostering interdisciplinary collaboration, we aim to identify key challenges, share best practices, and develop a roadmap for future research in this critical area.

Abstract
Safety-critical interactive systems pose design and evaluation challenges that go beyond usability. The safety of the system (i.e. the guarantee that it does not reach an undesirable or incorrect state) is also a relevant consideration. Traditional user-centred approaches (UCD) lack the rigour and thoroughness needed to address safety, and formal verification arises as a possible solution. Applying formal verification to a safety-critical interactive system design encompasses developing a model, expressing and verifying properties, and analysing the verification results. In the case of model checking, properties are typically expressed in temporal logic. This creates a gap between the languages used in UCD and the languages used for formal verification. Creating temporal logic properties manually requires expertise in formal methods and can be both time-consuming and error-prone. This paper explores how a patterns-based approach can be used to support the specification of properties in a natural language-based style. A prototype implementation of the approach is evaluated through a user study, and the results of this evaluation are discussed.

Abstract
With the rise of Transformers, Vision Transformers (ViTs) have become a new standard in visual recognition. This has led to the development of numerous architectures with diverse designs and applications. This survey identifies 22 key ViT and hybrid CNN–ViT models, along with 5 top Convolutional Neural Network (CNN) models. These were selected based on their new architecture, relevance to benchmarks, and overall impact. The models are organised using a defined taxonomy formed by CNN-based, pure Transformer-based, and hybrid architectures. We analyse their main components, training methods, and computational features, while assessing performance using reported results on standard benchmarks such as ImageNet and CIFAR, along with our training and fine-tuning evaluations on specific imaging datasets. In addition to accuracy, we look at real-world deployment issues by analysing the trade-offs between accuracy and efficiency in embedded, mobile, and clinical settings. The results indicate that modern CNNs are still very competitive in limited-resource environments, while advanced ViT variants perform well after large-scale pretraining, especially in areas with high variability. Hybrid CNN–ViT architectures, on the other hand, tend to offer the best balance between accuracy, data efficiency, and computational cost. This survey establishes a consolidated benchmark and reference framework for understanding the evolution, capabilities, and practical applicability of contemporary vision architectures. © © 2026. Published by Elsevier Ltd.