TEAL 2026 – DOMtutor: Automated Autograding for Logic in Computer Science

This website provides a small overview of DOMtutor in the context of teaching in logic as well as some example problems. DOMtutor is a set of scripts used to leverage the code autograder DOMjudge (popularly used for programming contests).

What is DOMjudge

In essence, DOMjudge allows participants to submit code to solve given problems. Problems are formal descriptions of the desired output together with a time limit. DOMjudge compiles submitted code and runs the executable in a sandboxed environment, checking its input/output behaviour (and time/memory consumption). As such, DOMjudge supports practically any programming language and any (computable) output check.

What is DOMtutor

DOMtutor provides utilities around DOMjudge to ease / automate management, especially for teaching contexts. The scripts allow declarative definitions of users, courses, etc. and preparing all necessary data for a lecture (lecture slides, problem descriptions & solutions, DOMjudge contest, solution statistics, etc.) are “push button”. For example, after an initial setup, synchronizing the list of participants from moodle, creating and uploading all problems used for a lecture week, exporting grades of all participants to moodle, or even generating nice statistics for presentation can be done in an instant. The tool is developed at GitHub.

Autograders for Logic

Autograders like DOMjudge are typically used in practically oriented lectures, teaching for example basics of programming, algorithms, or software engineering. However, autograders can (and, in my opion, should) also be used for lectures on theoretical computer science. For example, in parallel to learning about NFA-to-DFA determinization or DPLL, students can be tasked to actually implement the respective algorithm practically. Both anecdotal and scientific evidence suggests that such “hands-on” experience can significantly improve student learning.

Try it yourself!

As part of TEAL2026, you can try out such problemsolving yourself!

• Self register at the self-service (N.B.: This is very new, if there are any issues, please contact me!)
• Log in at the TEAL 2026 DOMjudge instance
• Attempt to solve the provided problems

Please note: The DOMjudge instance is running on my homeserver. There might be some downtimes.

To get you started, a solution to the “Hello World” problem in Python could look like this:

name_count = int(input())
for _ in range(name_count):
    name = input().strip()
    print(f"Ola {name}!")

Save this in a file and submit it at the DOMjudge instance for the “Hello World” problem. For the “Pastry Perfection” problem, a small template might be useful.

# Clauses are represented as sets of numbers, representing variables.
# Positive numbers represent the variable appearing positively, a negative number indicates negation.
# For example {-1, 2, 5} represents the clause !x_1 & x_2 & x_5.

def remove_unit_clause(clauses):
    # Propagate a unit clause (i.e. single-variable clause) if it exists:
    # Remove clauses that contain the variable, remove negation of the variable from the other clauses
    # Return True, modified_clauses if something has changed, otherwise return False, clauses
    pass


def pure_literal_assign(clauses):
    # Search for pure literals (those that appear only positively or only negatively) and assign them accordingly
    # Return True, modified_clauses if there was some change, and False, clauses otherwise
    pass


def dpll(clauses):
    while True:
        change, clauses = remove_unit_clause(clauses)
        if not change:
            break
    while True:
        change, clauses = pure_literal_assign(clauses)
        if not change:
            break
    if not clauses:
        return True
    if any(not cl for cl in clauses):
        return False
    literal = next(iter(clauses[0]))
    return dpll(clauses + [{literal}]) or dpll(clauses + [{-literal}])


m, n = map(int, input().split())
cs = [set(map(int, input().split()[:-1])) for _ in range(n)]
print('yes' if dpll(cs) else 'no')

Should you be interested in using DOMtutor for a lecture (in particular to teach algorithms & data structures) or anything else, feel free to talk to me at TEAL or contact me via email!