-
Measuring Item Similarity in Introductory Programming: Python and Robot Programming Case Studies
Authors:
Radek Pelánek,
Tomáš Effenberger,
Matěj Vaněk,
Vojtěch Sassmann,
Dominik Gmiterko
Abstract:
A personalized learning system needs a large pool of items for learners to solve. When working with a large pool of items, it is useful to measure the similarity of items. We outline a general approach to measuring the similarity of items and discuss specific measures for items used in introductory programming. Evaluation of quality of similarity measures is difficult. To this end, we propose an e…
▽ More
A personalized learning system needs a large pool of items for learners to solve. When working with a large pool of items, it is useful to measure the similarity of items. We outline a general approach to measuring the similarity of items and discuss specific measures for items used in introductory programming. Evaluation of quality of similarity measures is difficult. To this end, we propose an evaluation approach utilizing three levels of abstraction. We illustrate our approach to measuring similarity and provide evaluation using items from three diverse programming environments.
△ Less
Submitted 24 May, 2018;
originally announced June 2018.
-
Difficulty Rating of Sudoku Puzzles: An Overview and Evaluation
Authors:
Radek Pelánek
Abstract:
How can we predict the difficulty of a Sudoku puzzle? We give an overview of difficulty rating metrics and evaluate them on extensive dataset on human problem solving (more then 1700 Sudoku puzzles, hundreds of solvers). The best results are obtained using a computational model of human solving activity. Using the model we show that there are two sources of the problem difficulty: complexity of in…
▽ More
How can we predict the difficulty of a Sudoku puzzle? We give an overview of difficulty rating metrics and evaluate them on extensive dataset on human problem solving (more then 1700 Sudoku puzzles, hundreds of solvers). The best results are obtained using a computational model of human solving activity. Using the model we show that there are two sources of the problem difficulty: complexity of individual steps (logic operations) and structure of dependency among steps. We also describe metrics based on analysis of solutions under relaxed constraints -- a novel approach inspired by phase transition phenomenon in the graph coloring problem. In our discussion we focus not just on the performance of individual metrics on the Sudoku puzzle, but also on their generalizability and applicability to other problems.
△ Less
Submitted 28 March, 2014;
originally announced March 2014.
-
Predicate Abstraction with Under-approximation Refinement
Authors:
Corina S. Pasareanu,
Radek Pelanek,
Willem Visser
Abstract:
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while…
▽ More
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs.
△ Less
Submitted 26 February, 2007; v1 submitted 22 January, 2007;
originally announced January 2007.
