tensorlogic_ir/resolution/
proof.rs

1//! # Proof Result, Resolution Step, Strategy, and Statistics
2//!
3//! This module defines the supporting types used by the resolution prover:
4//! the outcome of a proof attempt, a single resolution step in a derivation,
5//! the available proof strategies, and the statistics gathered during
6//! proof search.
7
8use serde::{Deserialize, Serialize};
9
10use super::clause::Clause;
11use super::literal::Literal;
12
13/// Result of a resolution proof attempt.
14#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
15pub enum ProofResult {
16    /// The clause set is unsatisfiable (empty clause derived)
17    Unsatisfiable {
18        /// Steps taken to derive empty clause
19        steps: usize,
20        /// Derivation path (sequence of resolution steps)
21        derivation: Vec<ResolutionStep>,
22    },
23    /// The clause set is satisfiable (no contradiction found)
24    Satisfiable,
25    /// Proof attempt reached saturation without finding empty clause
26    Saturated {
27        /// Number of clauses generated
28        clauses_generated: usize,
29    },
30    /// Proof search reached resource limit
31    ResourceLimitReached {
32        /// Number of steps attempted
33        steps_attempted: usize,
34    },
35}
36
37impl ProofResult {
38    /// Check if the result proves unsatisfiability.
39    pub fn is_unsatisfiable(&self) -> bool {
40        matches!(self, ProofResult::Unsatisfiable { .. })
41    }
42
43    /// Check if the result proves satisfiability.
44    pub fn is_satisfiable(&self) -> bool {
45        matches!(self, ProofResult::Satisfiable)
46    }
47
48    /// Get the number of steps taken.
49    pub fn steps(&self) -> usize {
50        match self {
51            ProofResult::Unsatisfiable { steps, .. } => *steps,
52            ProofResult::ResourceLimitReached { steps_attempted } => *steps_attempted,
53            ProofResult::Saturated { clauses_generated } => *clauses_generated,
54            ProofResult::Satisfiable => 0,
55        }
56    }
57}
58
59/// A single resolution step in a proof.
60#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
61pub struct ResolutionStep {
62    /// First parent clause
63    pub parent1: Clause,
64    /// Second parent clause
65    pub parent2: Clause,
66    /// Resulting resolvent clause
67    pub resolvent: Clause,
68    /// Literal that was resolved on (from parent1)
69    pub resolved_literal: Literal,
70}
71
72/// Resolution proof strategy.
73#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
74pub enum ResolutionStrategy {
75    /// Generate all possible resolvents until empty clause or saturation
76    Saturation {
77        /// Maximum number of clauses to generate
78        max_clauses: usize,
79    },
80    /// Focus resolution on specific set of clauses
81    SetOfSupport {
82        /// Maximum resolution steps
83        max_steps: usize,
84    },
85    /// Only resolve with unit clauses (more efficient)
86    UnitResolution {
87        /// Maximum resolution steps
88        max_steps: usize,
89    },
90    /// Linear resolution: chain from initial clause
91    Linear {
92        /// Maximum chain length
93        max_depth: usize,
94    },
95}
96
97/// Statistics for resolution proof search.
98#[derive(Clone, Debug, Default, Serialize, Deserialize)]
99pub struct ProverStats {
100    /// Total clauses generated
101    pub clauses_generated: usize,
102    /// Resolution steps performed
103    pub resolution_steps: usize,
104    /// Tautologies removed
105    pub tautologies_removed: usize,
106    /// Clauses subsumed
107    pub clauses_subsumed: usize,
108    /// Empty clause found
109    pub empty_clause_found: bool,
110}
tensorlogic_ir/resolution/proof.rs

tensorlogic_ir/resolution/
proof.rs
