Z3Guide: A Scalable, Student-Centered, and Extensible Educational Environment for Logic Modeling
Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bj{\o}rner

TL;DR
Z3Guide is an open-source, scalable, and extensible educational platform designed to improve teaching and learning of logic modeling for CSPs, supporting diverse educational needs and enhancing student engagement.
Contribution
The paper introduces Z3Guide, a novel, student-centered, and extensible educational environment for logic modeling, developed through user-centered design and iterative feedback.
Findings
Positive student feedback on learning support
Effective implementation of design guidelines in Z3Guide
Identified opportunities for future educational improvements
Abstract
Constraint-satisfaction problems (CSPs) are ubiquitous, ranging from budgeting for grocery shopping to verifying software behavior. Logic modeling helps solve CSPs programmatically using SMT solvers. Despite its importance in many Computer Science disciplines, resources for teaching and learning logic modeling are scarce and scattered, and challenges remain in designing educational environments for logic modeling that are accessible and meet the needs of teachers and students. This paper explores how to design such an environment and probes the impact of the design on the learning experience. From a need-finding interview study and a design iteration with teachers of logic modeling, we curated 10 design guidelines spanning three main requirements: providing easy access, supporting various educational modalities, and allowing extensions for customized pedagogical needs. We implemented…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Scheduling and Timetabling Solutions · Logic, programming, and type systems
