Struct Solver 

pub struct Solver { /* private fields */ }

The CLS-based SAT/MaxSAT solver.

Implements Continuous Local Search, treating SAT as continuous optimization. Variables are relaxed from {0,1} to [0,1] and gradient descent with momentum is used to minimize the unsatisfied clause penalty.

Algorithm

The solver minimizes the “unsatisfied-ness” of clauses:

• For each clause, compute the product of (1 - lit_value) for all literals
• This product is 0 when any literal is satisfied, approaching 1 when all fail
• Gradient descent moves variables to minimize this penalty

Completeness

CLS is an incomplete solver - it can find satisfying assignments efficiently but cannot prove unsatisfiability. For unsatisfiable instances, it will return Unknown status with the best-effort assignment found.

Example

use xlog_solve::{SolveInstance, Clause, Literal, Solver, SolverConfig};

// Create instance: (x0 OR x1) AND (NOT x0 OR x1)
let instance = SolveInstance::new(2, vec![
    Clause::new(vec![Literal::positive(0), Literal::positive(1)]),
    Clause::new(vec![Literal::negative(0), Literal::positive(1)]),
]);

// Solve with default config
let solver = Solver::new_cpu();
let result = solver.solve(instance.clone());

// Or with custom config
let config = SolverConfig::default().with_max_iterations(5000);
let solver = Solver::with_config_cpu(config);
let result = solver.solve(instance);

Implementations

impl Solver

pub fn new_cpu() -> Self

Creates a new CPU-based CLS solver with default configuration.

Example

use xlog_solve::Solver;

let solver = Solver::new_cpu();

pub fn with_config_cpu(config: SolverConfig) -> Self

Creates a new CPU-based CLS solver with custom configuration.

Arguments

• config - The solver configuration

Example

use xlog_solve::{Solver, SolverConfig};

let config = SolverConfig::default()
    .with_max_iterations(5000)
    .with_learning_rate(0.05);
let solver = Solver::with_config_cpu(config);

pub fn config(&self) -> &SolverConfig

Returns a reference to the solver configuration.

pub fn solve(&self, instance: SolveInstance) -> SolveResult

Solves the given SAT instance.

Arguments

• instance - The SAT/MaxSAT instance to solve

Returns

A SolveResult containing:

• Sat status with satisfying assignment if found
• Unknown status with best-effort assignment if not found

Note: CLS cannot prove unsatisfiability, so Unsat is never returned.

Example

use xlog_solve::{SolveInstance, Clause, Literal, Solver, SolveStatus};

let instance = SolveInstance::new(1, vec![
    Clause::new(vec![Literal::positive(0)]),
]);

let solver = Solver::new_cpu();
let result = solver.solve(instance);

assert!(matches!(result.status, SolveStatus::Sat));

Trait Implementations

impl Clone for Solver

fn clone(&self) -> Solver

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Solver

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

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Self

Returns the “default value” for a type.