Skip to content

UnB-SAT/grounded-padlock

BranchesTags

Repository files navigation

🔒 Padlock Challenge

A complete system for generation, solving, explanation, and evaluation of "Padlock Challenge" logic puzzles.

📄 Supplementary material for the paper "A Neuro-Symbolic Framework for Logic Puzzle Solving: Pseudo-Boolean Reasoning with LLM-Based Explanations" — Bruno Cesar Ribas, Razer A. N. R. Montaño, Fabiano Silva, and Gabriel Tiveron — accepted at BRACIS 2026 (Brazilian Conference on Intelligent Systems).

This repository hosts the code, puzzle instances, prompts, generated explanations, and evaluation data used in the paper. A fully worked end-to-end example (structured clues → PB solver → solution-grounded analysis → exact prompts → real LLM output) is in WORKED_EXAMPLE.md.

Table of Contents

Overview

This project implements an end-to-end research pipeline:

┌──────────────┐    ┌──────────────┐    ┌──────────────┐    ┌──────────────┐
│  Instance    │───▶│  Solving     │───▶│  Explanation  │───▶│  Evaluation  │
│  Generation  │    │  (PB Solver) │    │  (LLMs)       │    │  (Human +    │
│              │    │              │    │               │    │   Automatic)  │
└──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘
  1. Generation: Creates puzzle instances with guaranteed unique solutions
  2. Solving: Encodes as Pseudo-Boolean formulas and solves with clasp
  3. Explanation: Generates natural language explanations via LLMs
  4. Evaluation: HTML forms for human evaluation + automatic verifier

Repository Structure

.
├── README.md                          # This file
├── enunciados/                        # Puzzle instances (.in files)
│   ├── imprimeitor.sh                 # Formats puzzles for human-readable display
│   ├── exemplo-2n.in                  # Example puzzle (2 digits)
│   ├── escape-3n.in                   # Puzzle with 3 digits
│   ├── padlock-4n.in                  # Puzzle with 4 digits
│   ├── genereitor-5n.in               # Puzzle with 5 digits
│   └── ...
├── formuleitor/                       # Solver engine and generators
│   ├── formuleitor.sh                 # Puzzle → PB formula encoder
│   ├── formuleitor-funcs.sh           # Encoder helper functions
│   ├── interpreteitor.sh              # Decodes clasp output → solution
│   ├── ambigueitor.sh                 # Checks ambiguity (multiple solutions)
│   ├── contasolucao.sh                # Counts total number of solutions
│   ├── traceitor.sh                   # Generates deduction trace (JSON)
│   ├── explicaitor.sh                 # Full LLM explanation pipeline
│   ├── explicaitor-offline.sh         # Generates prompt for manual LLM use
│   ├── benchmark-explicaitor.sh       # Runs batch explanations
│   ├── instance-generators.py         # Instance generators (Python)
│   ├── llm/
│   │   ├── explicaitor.py             # Python backend for LLM calls
│   │   └── prompt-template.txt        # Prompt template
│   └── cfiles/
│       ├── casual_generator.py        # Casual generator (C + Python)
│       ├── latin_square_genereitor.py # Latin square generator
│       ├── genereitor_bruteforce.py   # Brute force generator
│       └── imprimeitor.py             # Python formatter
├── evaluation/                        # Explanation evaluation
│   ├── generate-evaluation.sh         # Form generation orchestrator
│   ├── generate-evaluation.py         # Individual HTML form generator
│   ├── generate-evaluation-survey.py  # Multi-puzzle survey generator
│   ├── collect-responses.py           # Response collector and analyzer
│   ├── analyze-results.py             # Statistical analysis and LaTeX tables
│   ├── explanations/                  # Generated explanations (JSONs)
│   ├── analysis.json                  # Analysis results
│   └── instrucoes-uso.txt             # Usage instructions
└── pipeline-experiment.py             # Automated experiment pipeline

Prerequisites

Required

Tool Purpose Installation
bash ≥ 4.0 Shell scripts Included in Linux/macOS
Python ≥ 3.8 Generators, evaluation, pipeline apt install python3
clasp Pseudo-Boolean/ASP solver apt install clasp or potassco.org

Optional (for LLM explanations)

Tool Purpose Installation
openai (Python) GPT-4/5 API pip install openai
anthropic (Python) Claude API pip install anthropic
ollama Local LLMs (Llama, etc.) ollama.com
requests (Python) Ollama communication pip install requests

Environment Variables (for LLMs)

# OpenAI
export OPENAI_API_KEY="sk-..."

# Anthropic
export ANTHROPIC_API_KEY="sk-ant-..."

# Ollama (no variable needed, just needs to be running)
ollama serve &
ollama pull llama3.2

Quick Verification

# Check clasp
clasp --version

# Check Python
python3 --version

# Check optional dependencies
python3 -c "import openai; print('OpenAI OK')"
python3 -c "import anthropic; print('Anthropic OK')"
curl -s http://localhost:11434/api/tags | python3 -m json.tool

The Puzzle

The "Padlock Challenge" is a logic puzzle where the player must discover a secret code from clues. Each clue provides a guess along with three pieces of information:

  • How many digits are correct (present in the code)
  • How many are in the right place (correct position)
  • How many are in the wrong place (present but in a different position)

File Format (.in)

3                    ← number of digits in the code (holes)
5                    ← number of clues
682 1 1 0            ← guess: 682, 1 correct, 1 in right place, 0 in wrong place
614 1 0 1            ← guess: 614, 1 correct, 0 in right place, 1 in wrong place
206 2 0 2            ← guess: 206, 2 correct, 0 in right place, 2 in wrong place
738 0 0 0            ← guess: 738, nothing correct
780 1 0 1            ← guess: 780, 1 correct, 0 in right place, 1 in wrong place

Each clue line follows the format:

<guess> <correct_count> <right_place_count> <wrong_place_count>

Module: enunciados/

Contains ready-made puzzle instances and a formatter.

imprimeitor.sh

Formats a .in file for friendly human-readable display (in Portuguese).

Usage:

cd enunciados/
bash imprimeitor.sh < exemplo-2n.in

Output:

Menos de 5% acertam esse desafio!
Qual é a senha do 🔒 ?

O cadeado possui um senha com 2 dígitos não repetidos

Temos as seguintes dicas:
57 1 corretos, mas no lugar errado.
15 1 corretos, e no lugar certo.
83 nada está correto

File naming convention:

  • The suffix indicates size: *-2n.in = 2 digits, *-3n.in = 3 digits, etc.
  • The prefix indicates origin: escape, padlock, mathway, etc.

Module: formuleitor/

Core solver engine. Encodes puzzles as Pseudo-Boolean formulas and solves them with clasp.

formuleitor.sh

Encodes a .in puzzle into a Pseudo-Boolean formula (OPB format).

Usage:

cd formuleitor/
bash formuleitor.sh < ../enunciados/escape-3n.in

What it does:

  1. Reads the .in file (holes + clues)
  2. Creates boolean variables x_{digit}_{position} for every possible combination
  3. Generates constraints:
    • Exactly 1 digit per position
    • For each clue: constraints for correct-in-right-place and correct-in-any-place
    • Digits absent from all clues cannot be in the solution
  4. Outputs the formula in OPB format (readable by clasp)

Typical pipeline (solve a puzzle):

cd formuleitor/

# Encode → solve → interpret
bash formuleitor.sh < ../enunciados/escape-3n.in > /tmp/formula.opb
clasp /tmp/formula.opb > /tmp/solution.clasp
bash interpreteitor.sh ../enunciados/escape-3n.in < /tmp/solution.clasp

formuleitor-funcs.sh

Function library used by formuleitor.sh. Not meant to be executed directly.

Available functions:

Function Description
push_constraint Adds a constraint to the formula
push_comment Adds a comment to the formula
printformula Prints the complete OPB formula
getvarnumber Returns the variable index for a (digit, position) pair
generate_combinations Generates number combinations (helper)

interpreteitor.sh

Decodes clasp output into a human-readable solution.

Usage:

cd formuleitor/
bash formuleitor.sh < ../enunciados/escape-3n.in > /tmp/formula.opb
clasp /tmp/formula.opb | bash interpreteitor.sh ../enunciados/escape-3n.in

Output:

0 4 2

Arguments:

  • $1: original problem file (needed to reconstruct the variable map)
  • stdin: clasp output

ambigueitor.sh

Checks whether a puzzle has multiple solutions and lists all of them.

Usage:

cd formuleitor/
bash ambigueitor.sh ../enunciados/escape-3n.in

Output (unique solution):

Base solution:
0 4 2

Checking for aditional solutions...
  Removing x43
  Removing x101
  Removing x22

Aditional solutions count: 0

Output (ambiguous solution):

Base solution:
1 2 3

Checking for aditional solutions...
  Removing x11
    4 2 3
  Removing x22
    1 5 3

Aditional solutions count: 2

How it works:

  1. Finds a base solution
  2. For each true variable, forces it to false and re-solves
  3. If a new solution is found, counts it as additional
  4. Reports the total extra solution count

contasolucao.sh

Counts the total number of solutions using clasp 0 (enumerate all models).

Usage:

cd formuleitor/
bash contasolucao.sh ../enunciados/escape-3n.in

Output:

Models       : 1

Note: More efficient than ambigueitor.sh when only the count is needed.

traceitor.sh

Generates a complete deduction trace in JSON format.

Usage:

cd formuleitor/
bash traceitor.sh ../enunciados/escape-3n.in

Output (JSON):

{
    "status": "SATISFIABLE",
    "holes": 3,
    "solution": "042",
    "solution_array": [0, 4, 2],
    "clues": [
        {
            "id": 0,
            "guess": "682",
            "feedback": {
                "correct": 1,
                "well_placed": 1,
                "wrong_placed": 0
            },
            "analysis": {
                "digits_in_solution": ["2"],
                "well_placed": ["2:2"],
                "wrong_placed": [],
                "eliminated": ["6", "8"]
            }
        }
    ],
    "deduction_summary": {
        "eliminated_digits": [1, 3, 5, 6, 7, 8, 9],
        "solution_digits": [0, 4, 2]
    }
}

Key fields:

  • analysis.eliminated: digits from the guess that are NOT in the solution
  • analysis.well_placed: correct digits in the right position ("digit:position")
  • analysis.wrong_placed: correct digits in wrong position ("digit:guess_pos->real_pos")

Arguments:

  • $1: problem file
  • $2 (optional): file with clasp output (if omitted, runs the solver internally)

explicaitor.sh

Full pipeline: trace → prompt → LLM → natural language explanation.

Usage:

cd formuleitor/
bash explicaitor.sh ../enunciados/escape-3n.in
bash explicaitor.sh ../enunciados/escape-3n.in --theme spy
bash explicaitor.sh ../enunciados/escape-3n.in --theme fantasy --level partial
bash explicaitor.sh ../enunciados/escape-3n.in --json

Parameters:

Parameter Values Default Description
--theme neutral, spy, fantasy, scifi neutral Thematic style of the explanation
--level full, partial, minimal full Level of detail
--json (flag) off JSON output instead of text

Themes:

  • neutral: Educational logic tutor
  • spy: Spy agency analyst decoding an intercepted transmission
  • fantasy: Ancient wizard deciphering magical runes
  • scifi: Starship computer analyzing alien sequences

Internal pipeline:

puzzle.in → traceitor.sh → JSON → explicaitor.py → LLM API → explanation

Requires: At least one LLM backend configured (OpenAI, Anthropic, or Ollama).

explicaitor-offline.sh

Generates only the prompt for manual use with any LLM (ChatGPT web, Claude web, etc.).

Usage:

cd formuleitor/
bash explicaitor-offline.sh ../enunciados/escape-3n.in > prompt.txt
# Copy the contents of prompt.txt into your preferred LLM
cat prompt.txt

Useful when:

  • No API key is configured
  • You want to use an LLM's web interface
  • You want to manually customize the prompt

benchmark-explicaitor.sh

Runs explanations in batch for all instances and all themes.

Usage:

cd formuleitor/
bash benchmark-explicaitor.sh

What it does:

  • Iterates over all *.in files in ../enunciados/
  • For each instance, generates an explanation with every theme (neutral, spy, fantasy, scifi)
  • Saves results to ./results/

instance-generators.py

Instance generator with guaranteed unique solution. Implements 3 strategies.

Basic usage:

cd formuleitor/

# Casual generator (recommended)
python3 instance-generators.py --generator casual --holes 4 --clues 5

# Latin square generator
python3 instance-generators.py --generator latin --holes 5 --clues 6

# Custom alphabet
python3 instance-generators.py --generator casual --holes 4 \
    --alphabet alphanumeric --alphabet-size 20 --clues 6

# Generate multiple instances
python3 instance-generators.py --generator casual --holes 4 \
    --count 10 --output-dir ./instances --format both

# Comparative benchmark of generators
python3 instance-generators.py --benchmark --repetitions 5

Generation strategies:

Strategy Description Speed Recommendation
bruteforce Completely random clues and feedback Very slow Comparison only
casual Picks secret, generates correct feedback, validates uniqueness Fast General use
latin Uses Latin square structure for more diverse guesses Fast Larger puzzles

Full parameters:

Parameter Description Default
--generator, -g Strategy: bruteforce, casual, latin casual
--holes, -H Number of positions in the code 3
--clues, -c Initial number of clues to generate 5
--alphabet, -a Alphabet type digits
--alphabet-size, -s Limit alphabet size (full type)
--no-repetition Disallow repeated digits off
--count, -n Number of instances to generate 1
--output, -o Output file path stdout
--output-dir Directory for multiple instances —
--format, -f Format: in, json, both in
--max-attempts Maximum generation attempts 100
--seed Seed for reproducibility random
--solver Solver command clasp
--verbose, -v Detailed progress off
--benchmark, -b Comparative benchmark mode off
--repetitions, -r Benchmark repetitions 5

Alphabet types:

Type Symbols Size
digits 0-9 10
lowercase a-z 26
uppercase A-Z 26
letters a-zA-Z 52
alphanumeric 0-9a-zA-Z 62
alphanumeric_lower 0-9a-z 36
alphanumeric_upper 0-9A-Z 36

Uniqueness guarantee: All strategies use clasp 2 (search for up to 2 models) to verify uniqueness in a single solver call.

llm/explicaitor.py

Python backend for LLM-based explanation generation. Called by explicaitor.sh but can also be used directly.

Direct usage:

cd formuleitor/

# Via pipe from traceitor
bash traceitor.sh ../enunciados/escape-3n.in | \
    python3 llm/explicaitor.py --theme neutral --level full

# With trace file
python3 llm/explicaitor.py --trace trace.json --theme spy --output json

Parameters:

Parameter Description Default
--trace, -t Path to trace JSON (or stdin) stdin
--theme Theme: neutral, spy, fantasy, scifi neutral
--level Detail: full, partial, minimal full
--output, -o Format: json, text text

Automatic backend detection: Tries OpenAI → Anthropic → Ollama, in order, using the first one available.

cfiles/ (Legacy Python/C Generators)

Alternative generators that depend on a C executable (padlock_challenge).

casual_generator.py

Guided random generator that uses the C solver for validation.

cd formuleitor/cfiles/
python3 casual_generator.py 4 15   # 4 digits, 15-symbol dictionary

latin_square_genereitor.py

Latin square generator using the C solver.

cd formuleitor/cfiles/
python3 latin_square_genereitor.py 4 15

genereitor_bruteforce.py

Pure brute force generator (very slow).

cd formuleitor/cfiles/
python3 genereitor_bruteforce.py

imprimeitor.py

Python puzzle formatter with terminal colors.

cd formuleitor/cfiles/
python3 imprimeitor.py < ../teste.in

Note: The generators in cfiles/ require the padlock_challenge executable compiled separately. The recommended main generator is instance-generators.py.

Module: evaluation/

Tools for human and automatic evaluation of explanations.

generate-evaluation.sh

Shell orchestrator for evaluation form generation.

Usage:

cd evaluation/

# Demo mode (generates example)
bash generate-evaluation.sh

# Single instance
bash generate-evaluation.sh --instance ../enunciados/escape-3n.in

# Batch (all instances)
bash generate-evaluation.sh --batch

# With specific language and themes
bash generate-evaluation.sh --batch --lang pt --themes "neutral spy"

Parameters:

Parameter Description
--batch, -b Process all instances in ../enunciados/
--instance, -i Process a specific instance
--lang, -l Language: en or pt
--themes, -t Themes (space-separated)
--output, -o Output directory

generate-evaluation.py

Generates individual HTML forms for explanation evaluation.

Usage:

cd evaluation/

# Demo mode
python3 generate-evaluation.py

# Single instance
python3 generate-evaluation.py \
    --instance ../enunciados/escape-3n.in \
    --explanation ./explanations/escape-3n_neutral.json \
    --output-dir ./forms --lang en

# Batch
python3 generate-evaluation.py \
    --instances-dir ../enunciados \
    --explanations-dir ./explanations \
    --output-dir ./forms \
    --lang en --themes neutral spy fantasy scifi

Evaluation criteria (1–5 scale):

  1. Correctness — Are the deduction steps valid?
  2. Completeness — Are all important steps included?
  3. Clarity — Is the explanation easy to understand?
  4. Usefulness — Would it be useful as a hint in a game?

Additional questions:

  • Theme appropriateness (only for non-neutral themes)
  • "Would you use this in a game?" (yes/no)
  • Free-text comments

Output: Interactive HTML forms with:

  • Puzzle and solution display
  • Clickable Likert scale
  • JSON export (copy, download, or email)
  • Index page with links to all forms
  • CSV for Google Forms import

generate-evaluation-survey.py

Generates a complete multi-puzzle survey in a single HTML page.

Usage:

cd evaluation/

# Demo
python3 generate-evaluation-survey.py --output survey.html --lang en

# With real instances
python3 generate-evaluation-survey.py \
    --instances-dir ../enunciados \
    --explanations-dir ./explanations \
    --output survey.html \
    --lang en \
    --themes neutral spy fantasy

Survey features:

  • Dot navigation between puzzles
  • Real-time progress (answered / skipped / remaining)
  • Option to skip puzzles
  • Hidden solution (hover/tap to reveal)
  • Review screen before finishing
  • Full JSON export
  • Keyboard shortcuts (← → Enter)
  • Mobile responsive

Expected explanation JSON format:

{
    "solution": "042",
    "explanation": "Step 1: ..."
}

Naming convention: The script looks for explanations matching the pattern: {puzzle_name}_{theme}.json

Example: for escape-3n.in with theme neutral, it looks for escape-3n_neutral.json.

collect-responses.py

Collects, consolidates, and analyzes responses from evaluation forms.

Usage:

cd evaluation/

# Process specific files
python3 collect-responses.py \
    --input response1.json response2.json \
    --output results.csv

# Process entire directory
python3 collect-responses.py \
    --input-dir ./responses \
    --output results.csv

# Full analysis
python3 collect-responses.py \
    --input-dir ./responses \
    --output results.csv \
    --output-json analysis.json \
    --output-latex tables.tex \
    --summary

Accepted input formats:

  • Multi-puzzle survey JSON (with meta and evaluations)
  • Individual evaluation JSON (with instance_id and correctness)
  • List of evaluations

Output:

File Description
results.csv All evaluations in tabular format
analysis.json Statistics by criterion, theme, evaluator, and instance
tables.tex Paper-ready LaTeX tables

Generated statistics:

  • Mean, standard deviation, min, max, median
  • Grouping by theme, evaluator, and instance
  • "Would use in game" rate

analyze-results.py

In-depth statistical analysis for paper inclusion.

Usage:

cd evaluation/

python3 analyze-results.py \
    --input results.csv \
    --output-latex tables.tex \
    --output-summary summary.txt

Generates:

  • Formatted LaTeX tables (overall and by theme)
  • Summary text for the results section
  • Best/worst criterion identification

Experiment Pipeline

pipeline-experiment.py

Unified script that runs the complete research experiment.

Overview:

Step 1: Generate 50 instances (10 × 5 sizes, via Latin square)
    ↓
Step 2: Submit to 3 LLMs × 2 conditions = 300 explanations
    ↓
Step 3: Automatically verify all explanations

Step 1: Generation

python3 pipeline-experiment.py --generate
  • Generates 50 instances: 10 for each $H \in {3, 4, 5, 6, 7}$
  • Alphabet: digits 0–9 ($|\Sigma| = 10$)
  • Strategy: Latin square
  • Guarantees unique solution with clasp 2
  • Fixed seed for reproducibility

Output:

experiment/
├── instances/
│   ├── H3_inst01.in          # Puzzle file
│   ├── H3_inst01.json        # Metadata
│   ├── H3_inst02.in
│   └── ...
├── traces/
│   ├── H3_inst01_trace.json  # Deduction trace
│   └── ...
└── instances_manifest.json   # Manifest with all instances

Step 2: Submission

# Dry run (tests prompts without calling LLMs)
python3 pipeline-experiment.py --submit --dry-run

# Real submission
python3 pipeline-experiment.py --submit

Configured LLMs:

ID Backend Model
gpt-4o-mini OpenAI gpt-4o-mini
claude-3-haiku Anthropic claude-3-haiku-20240307
llama3.2 Ollama llama3.2

Experimental conditions:

Condition Description
grounded Prompt includes complete solver trace (eliminated digits, well-placed, etc.)
ungrounded Prompt includes only the puzzle and the solution (no trace)

Features:

  • Automatic resume (progress tracking in submission_progress.json)
  • Rate limiting (1s between calls)
  • Automatic backend availability detection
  • Error handling with logging

Output:

experiment/
└── explanations/
    ├── H3_inst01_gpt-4o-mini_grounded.json
    ├── H3_inst01_gpt-4o-mini_ungrounded.json
    ├── H3_inst01_claude-3-haiku_grounded.json
    └── ...  (300 files)

Step 3: Verification

python3 pipeline-experiment.py --verify

Checks performed (regex + keyword matching):

Check Method Metrics
Solution digits Searches for contextual mention of each digit Coverage (recall)
Eliminations Extracts digits the explanation claims to eliminate; compares with trace Precision and recall
Clue references Detects mentions by number or by the clue's guess Coverage
Final answer Extracts final numeric sequence; compares with solution Correct/incorrect
Positioning Extracts "position X = digit Y" claims; validates List of correct/incorrect

Regex patterns used:

  • Eliminations: eliminat|remov|discard|rule out|not in|cannot be|nada.*correto|...
  • References: clue|dica|hint|tip #?\d+
  • Final answer: solution|answer|code is|: \d{2,10} and **\d{2,10}**
  • Positioning: position \d is \d and variations

Composite scores:

Correctness (0–1):

  • 30% elimination precision
  • 40% final answer correct
  • 30% positional precision

Completeness (0–1):

  • 30% solution digit coverage
  • 30% elimination recall
  • 20% clue reference coverage
  • 20% final answer present

Output:

experiment/
├── verification/
│   ├── H3_inst01_gpt-4o-mini_grounded_verification.json
│   └── ...
└── results/
    ├── verification_results.csv      # All verifications (tabular)
    ├── verification_summary.json     # Aggregated statistics
    ├── verification_detailed.json    # Full detailed results
    └── verification_tables.tex       # LaTeX tables for the paper

Full Pipeline

# All steps at once
python3 pipeline-experiment.py --all

# With custom seed
python3 pipeline-experiment.py --all --seed 123

Configuration Customization

Edit EXPERIMENT_CONFIG at the top of the script:

EXPERIMENT_CONFIG = {
    "holes_values": [3, 4, 5, 6, 7],     # Code sizes
    "instances_per_holes": 10,             # Instances per size
    "alphabet_size": 10,                   # Alphabet size
    "alphabet": list(string.digits),       # Symbols

    "llm_models": [                        # LLMs to use
        {"id": "gpt-5.4", "backend": "openai", "model_name": "gpt-5.4"},
        {"id": "claude-3-haiku", "backend": "anthropic", "model_name": "claude-3-haiku-20240307"},
        {"id": "llama3.2", "backend": "ollama", "model_name": "llama3.2"},
    ],

    "conditions": ["grounded", "ungrounded"],
    "temperature": 0.7,
    "max_tokens": 3000,
    "seed": 42,
}

Quick Start

1. Solve an existing puzzle

cd formuleitor/
bash formuleitor.sh < ../enunciados/escape-3n.in > /tmp/f.opb
clasp /tmp/f.opb | bash interpreteitor.sh ../enunciados/escape-3n.in

2. Check if a puzzle is ambiguous

cd formuleitor/
bash ambigueitor.sh ../enunciados/escape-3n.in

3. Generate a new instance

cd formuleitor/
python3 instance-generators.py -g casual -H 4 -c 6 -o new_puzzle --format both

4. Generate an explanation via LLM

cd formuleitor/
# With LLM
bash explicaitor.sh ../enunciados/escape-3n.in --theme neutral

# Without LLM (generates prompt for manual use)
bash explicaitor-offline.sh ../enunciados/escape-3n.in > prompt.txt

5. Generate an evaluation form

cd evaluation/
python3 generate-evaluation-survey.py \
    --instances-dir ../enunciados \
    --explanations-dir ./explanations \
    --output survey.html --lang en
# Open survey.html in a browser

6. Analyze responses

cd evaluation/
python3 collect-responses.py \
    --input-dir ./responses \
    --output results.csv \
    --output-json analysis.json \
    --output-latex tables.tex \
    --summary

7. Run the full experiment

python3 pipeline-experiment.py --all

Full Examples

Example 1: From scratch to explanation

# 1. Generate puzzle
cd formuleitor/
python3 instance-generators.py \
    --generator latin \
    --holes 4 \
    --clues 6 \
    --output ../enunciados/my_puzzle \
    --format both

# 2. Verify uniqueness
bash contasolucao.sh ../enunciados/my_puzzle.in

# 3. Display
bash ../enunciados/imprimeitor.sh < ../enunciados/my_puzzle.in

# 4. Generate trace
bash traceitor.sh ../enunciados/my_puzzle.in > /tmp/trace.json

# 5. Generate explanation
bash explicaitor.sh ../enunciados/my_puzzle.in --theme neutral

Example 2: Batch evaluation

# 1. Generate explanations for all instances
cd formuleitor/
for f in ../enunciados/*.in; do
    name=$(basename "$f" .in)
    echo "Processing: $name"
    bash explicaitor.sh "$f" --json > \
        ../evaluation/explanations/${name}_neutral.json
done

# 2. Generate survey
cd ../evaluation/
python3 generate-evaluation-survey.py \
    --instances-dir ../enunciados \
    --explanations-dir ./explanations \
    --output survey.html \
    --lang en \
    --themes neutral

# 3. Open in browser and evaluate
xdg-open survey.html  # Linux
open survey.html       # macOS

# 4. After collecting responses (JSONs saved by the survey)
python3 collect-responses.py \
    --input-dir ./responses \
    --output results.csv \
    --output-json analysis.json \
    --output-latex tables.tex \
    --summary

Example 3: Reproducible experiment

# Deterministic generation
python3 pipeline-experiment.py --generate --seed 42

# Submission (can be resumed if interrupted)
python3 pipeline-experiment.py --submit

# Verification
python3 pipeline-experiment.py --verify

# Results will be in experiment/results/
cat experiment/results/verification_summary.json | python3 -m json.tool

Troubleshooting

clasp not found

ERROR: 'clasp' not found. Install clasp.

Solution:

# Ubuntu/Debian
sudo apt install clasp

# macOS (Homebrew)
brew install clasp

# Or compile from source:
# https://github.com/potassco/clasp

No LLM backend available

Error: No LLM backend available.

Solution: Configure at least one backend:

# Option 1: OpenAI
export OPENAI_API_KEY="sk-..."
pip install openai

# Option 2: Anthropic
export ANTHROPIC_API_KEY="sk-ant-..."
pip install anthropic

# Option 3: Ollama (free, local)
curl -fsSL https://ollama.com/install.sh | sh
ollama pull llama3.2

max_tokens error with recent OpenAI models

Unsupported parameter: 'max_tokens' is not supported with this model.
Use 'max_completion_tokens' instead.

Solution: The pipeline-experiment.py already handles this case automatically. If using explicaitor.py directly, update the call_openai function to use max_completion_tokens for GPT-5+/o1/o3/o4 models.

Survey cannot find explanations

ERROR: No valid instances found!

Solution: Verify that explanation JSON files follow the naming pattern:

explanations/{puzzle_name}_{theme}.json

And that each file contains at least:

{"solution": "042", "explanation": "...text..."}

Puzzle is UNSATISFIABLE

If the solver returns UNSATISFIABLE, the clues are inconsistent. Check:

  • Is the .in file well-formatted?
  • Are the correct/position counts coherent?
  • Use ambigueitor.sh for diagnostics.

Solver timeout

For large puzzles ($H &gt; 7$, $|\Sigma| &gt; 20$), the solver may take a long time. Options:

  • Increase the timeout in pipeline-experiment.py (the timeout variable in subprocess.run calls)
  • Reduce the alphabet size
  • Use fewer clues (the solver is faster with fewer constraints)

References

If you use this material, please cite the paper:

  • Ribas, B. C., Montaño, R. A. N. R., Silva, F., & Tiveron, G. (2026). A Neuro-Symbolic Framework for Logic Puzzle Solving: Pseudo-Boolean Reasoning with LLM-Based Explanations. In: Proceedings of the Brazilian Conference on Intelligent Systems (BRACIS 2026). To appear.

Key references cited in the paper (see the paper's bibliography for the full list):

  • clasp (PB solver used here): Gebser, M., Kaufmann, B., & Schaub, T. (2012). Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187, 52–89. potassco.org
  • Pseudo-Boolean constraints / SAT: Biere, A., Heule, M., van Maaren, H., & Walsh, T. (eds.) (2021). Handbook of Satisfiability (2nd ed.). IOS Press.
  • Mastermind (related code-breaking puzzle): Knuth, D. E. (1977). The Computer as Master Mind. Journal of Recreational Mathematics, 9(1), 1–6.
  • Neuro-Symbolic AI: Garcez, A. d'Avila, & Lamb, L. C. (2023). Neurosymbolic AI: The 3rd Wave. Artificial Intelligence Review, 56(11), 12387–12406.

About

A Neuro-Symbolic Framework for Logic Puzzle Solving: Pseudo-Boolean Reasoning with LLM-Based Explanations

Resources

Readme
Activity
Custom properties

Stars

0 stars

Watchers

3 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages