Treesolve

A SAT-based natural deduction proof validator and generator.

Overview

Treesolve encodes natural deduction proofs as SAT problems, enabling:

• Validation: Check if a given proof is valid
• Generation: Find proof completions for partial proofs

Architecture

The encoding represents proof rows as bit-vectors with:

• Type bits: Encode the class (Statement/ProofStep/Null) and kind (sentence type or rule)
• Pointer arrays: Reference other rows (conclusions, premises, discharged assumptions)
• Auxiliary variables: Helper variables for constraint propagation

Key Modules

• encoding: Core SAT representation with variables, clauses, and encoding/decoding
• sat: SAT primitives (Variable, Literal, Clause, DIMACS generation)
• runner: SAT solver integration (requires solver features)

Split Mode

The encoding uses a split row model controlled by Dimensions:

• Statement rows (indices 0..max_statement_rows): Can only hold Sentence or Null classes
• Proof rows (indices max_statement_rows..max_rows): Can hold ProofStep or Null classes (with full pointer arrays)

The split is controlled by the max_statement_rows parameter:

• max_statement_rows > 0: Rows are split between statement and proof regions
• max_statement_rows = 0: All rows are proof-capable (uniform mode)

Statement rows require fewer SAT variables since they don't need discharge/undischarged pointer arrays. This reduces the SAT problem size when many sentences are needed but fewer proof steps.

For the CLI, use --statement-rows and --proof-rows to control the split:

# Split mode: 10 statement rows, 5 proof rows
treesolve complexity -s 10 -p 5

# Uniform mode: all 15 rows are proof-capable  
treesolve complexity -s 0 -p 15

Testing

Run all tests:

cargo test

Run tests for a specific module:

cargo test encoding::constraints::tests
cargo test encoding::layout::dimensions::tests

Debug Assertions

The OffsetSchema::validate() method is available under debug_assertions or test configurations. It validates that all offset calculations produce unique, non-overlapping offsets.

This validation runs automatically in debug builds and tests. To explicitly test offset validation:

# Run in debug mode (default for `cargo test`)
cargo test test_offset_validation

# Run with debug assertions enabled in release mode
RUSTFLAGS="--cfg debug_assertions" cargo test --release test_offset_validation

The validation tests include:

• test_offset_validation_small: Small dimensions
• test_offset_validation_proof_only: No statement rows
• test_offset_validation_split_mode: Mixed statement and proof rows
• test_offset_validation_minimal: Minimal dimensions

Features

SAT solver features (at least one required for validation/generation):

• cadical: CaDiCaL solver
• glucose: Glucose solver
• lingeling: Lingeling solver
• minisat: MiniSat solver
• kissat: Kissat solver

Example:

cargo test --features cadical

Pointer Semantics

Pointers come in pairs (statement_ptr, proof_ptr) for discharge and undischarged arrays. Even indices point to statements, odd indices point to proof steps.

See encoding::layout::pointers for semantic constants that replace magic numbers:

• proof_step::CONCLUSION, PREMISE_1_STMT, PREMISE_2_STMT, etc.
• sentence::LEFT, RIGHT, ANTECEDENT, CONSEQUENT
• pairs::stmt_idx(), pairs::proof_idx() for pointer pair conventions