Enum SolveProof 

pub enum SolveProof {
    Satisfying {
        assignment: Vec<bool>,
        checksum: u64,
    },
    Unsatisfiable {
        checksum: u64,
    },
    Approximate {
        assignment: Vec<bool>,
        satisfied_clauses: u32,
        total_clauses: u32,
        iterations: u32,
    },
    None,
}

Proof artifact from a SAT/MaxSAT solver.

Proofs provide evidence of the solver’s conclusion. For satisfiable instances, this includes the satisfying assignment with a checksum for verification. For unsatisfiable instances, a proof of unsatisfiability is included.

Variants

• Satisfying: Contains a satisfying assignment with checksum
• Unsatisfiable: Proof that no satisfying assignment exists
• Approximate: Best-effort assignment that may not satisfy all clauses
• None: No proof available (e.g., timeout before any result)

Checksums

The checksum field uses FNV-1a hashing to enable lightweight verification that an assignment hasn’t been corrupted. This is particularly useful for:

• Verifying GPU-to-CPU transfers
• Detecting memory corruption
• Validating serialized/deserialized results

Example

use xlog_solve::SolveProof;

// Create a satisfying proof with automatic checksum
let proof = SolveProof::satisfying(vec![true, false, true]);
assert!(proof.is_satisfying());

// Extract the assignment
if let Some(assignment) = proof.assignment() {
    assert_eq!(assignment, &[true, false, true]);
}

Variants

Satisfying

The instance is satisfiable with the given assignment.

The checksum can be used to verify the assignment’s integrity.

Fields

assignment: Vec<bool>

The satisfying assignment (one boolean per variable).

checksum: u64

FNV-1a checksum of the assignment for integrity verification.

Unsatisfiable

The instance is unsatisfiable.

The checksum can be used to verify the proof’s integrity (e.g., if the solver produces resolution proofs).

Fields

checksum: u64

Checksum for proof integrity verification.

Approximate

An approximate solution from an incomplete solver.

This is typically produced by local search or heuristic solvers that may not find a complete satisfying assignment.

Fields

assignment: Vec<bool>

The best assignment found.

satisfied_clauses: u32

Number of clauses satisfied by this assignment.

total_clauses: u32

Total number of clauses in the instance.

iterations: u32

Number of solver iterations performed.

None

No proof available.

This occurs when the solver times out or is interrupted before producing any meaningful result.

Implementations

impl SolveProof

pub fn satisfying(assignment: Vec<bool>) -> Self

Creates a satisfying proof with automatic checksum computation.

Arguments

• assignment - The satisfying assignment

Example

use xlog_solve::SolveProof;

let proof = SolveProof::satisfying(vec![true, false, true]);
assert!(proof.is_satisfying());

pub fn unsatisfiable() -> Self

Creates an unsatisfiability proof.

The checksum is computed as a sentinel value for the empty proof.

Example

use xlog_solve::SolveProof;

let proof = SolveProof::unsatisfiable();
assert!(!proof.is_satisfying());

pub fn approximate( assignment: Vec<bool>, satisfied_clauses: u32, total_clauses: u32, iterations: u32, ) -> Self

Creates an approximate solution proof.

This is typically used by incomplete solvers (like local search) that may not find a fully satisfying assignment.

Arguments

• assignment - The best assignment found
• satisfied_clauses - Number of clauses satisfied
• total_clauses - Total number of clauses
• iterations - Number of solver iterations performed

Example

use xlog_solve::SolveProof;

let proof = SolveProof::approximate(vec![true, false], 8, 10, 1000);
if let SolveProof::Approximate { satisfied_clauses, total_clauses, .. } = proof {
    assert_eq!(satisfied_clauses, 8);
    assert_eq!(total_clauses, 10);
}

pub fn is_satisfying(&self) -> bool

Returns true if this is a satisfying proof.

Example

use xlog_solve::SolveProof;

assert!(SolveProof::satisfying(vec![true]).is_satisfying());
assert!(!SolveProof::unsatisfiable().is_satisfying());

pub fn assignment(&self) -> Option<&[bool]>

Returns the assignment if this proof contains one.

Returns Some for Satisfying and Approximate variants, None otherwise.

Example

use xlog_solve::SolveProof;

let proof = SolveProof::satisfying(vec![true, false]);
assert_eq!(proof.assignment(), Some(&[true, false][..]));

let unsat = SolveProof::unsatisfiable();
assert_eq!(unsat.assignment(), None);

pub fn checksum(&self) -> Option<u64>

Returns the checksum if this proof has one.

Example

use xlog_solve::SolveProof;

let proof = SolveProof::satisfying(vec![true]);
assert!(proof.checksum().is_some());

pub fn verify_checksum(&self) -> Option<bool>

Verifies the integrity of a satisfying assignment by recomputing its checksum.

Returns true if the checksum matches, false if corrupted. Returns None for non-satisfying proofs.

Example

use xlog_solve::SolveProof;

let proof = SolveProof::satisfying(vec![true, false]);
assert_eq!(proof.verify_checksum(), Some(true));

pub fn satisfaction_ratio(&self) -> Option<f64>

Returns the satisfaction ratio for approximate proofs.

Returns Some(ratio) for Approximate where ratio = satisfied_clauses / total_clauses. Returns None for other variants.

Example

use xlog_solve::SolveProof;

let proof = SolveProof::approximate(vec![true], 8, 10, 100);
assert_eq!(proof.satisfaction_ratio(), Some(0.8));

Trait Implementations

impl Clone for SolveProof

fn clone(&self) -> SolveProof

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SolveProof

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SolveProof

fn default() -> SolveProof

Returns the “default value” for a type.

impl Eq for SolveProof

impl PartialEq for SolveProof

fn eq(&self, other: &SolveProof) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SolveProof