Struct SolveInstance

Source

pub struct SolveInstance {
    pub num_vars: u32,
    pub clauses: Vec<Clause>,
    pub weights: Option<Vec<f64>>,
    pub objective: Objective,
}

Expand description

A SAT or MaxSAT instance in Conjunctive Normal Form (CNF).

This struct represents the complete problem to be solved:

A set of propositional variables (indexed 0 to num_vars-1)
A conjunction of clauses (each clause is a disjunction of literals)
Optional weights for MaxSAT
An optimization objective

§CNF Semantics

The formula represented is:

clause[0] AND clause[1] AND ... AND clause[n-1]

where each clause is:

lit[0] OR lit[1] OR ... OR lit[k-1]

§Memory Layout

The instance is designed for efficient GPU transfer:

Clauses can be flattened to a contiguous literal array with offset indices
Weights align with clause indices for vectorized operations

§Example

use xlog_solve::{SolveInstance, Clause, Literal, Objective};

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

assert_eq!(instance.num_vars, 3);
assert_eq!(instance.clauses.len(), 2);
assert_eq!(instance.objective, Objective::Satisfaction);

Fields§

§num_vars: u32

Number of propositional variables in this instance.

Variables are indexed from 0 to num_vars - 1.

§clauses: Vec<Clause>

The clauses forming this CNF formula.

The formula is satisfied when ALL clauses are satisfied.

§weights: Option<Vec<f64>>

Optional weights for each clause (for weighted MaxSAT).

If Some, must have the same length as clauses. If None, all clauses have implicit weight 1.0.

§objective: Objective

The optimization objective.

Implementations§

Source §

impl SolveInstance

Source

pub fn new(num_vars: u32, clauses: Vec<Clause>) -> Self

Creates a new SAT instance with the given variables and clauses.

The instance uses Objective::Satisfaction (standard SAT).

§Arguments

num_vars - The number of propositional variables
clauses - The clauses forming the CNF formula

§Example

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

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

Source

pub fn with_weights( num_vars: u32, clauses: Vec<Clause>, weights: Vec<f64>, ) -> Self

Creates a weighted MaxSAT instance.

§Arguments

num_vars - The number of propositional variables
clauses - The clauses forming the CNF formula
weights - Weights for each clause (must match clause count)

§Panics

Panics if weights.len() != clauses.len().

§Example

use xlog_solve::{SolveInstance, Clause, Literal, Objective};

let instance = SolveInstance::with_weights(
    2,
    vec![
        Clause::new(vec![Literal::positive(0)]),
        Clause::new(vec![Literal::positive(1)]),
    ],
    vec![1.0, 2.0],  // Clause 1 has twice the weight
);

assert_eq!(instance.objective, Objective::MaxSat);

Source

pub fn add_clause(&mut self, clause: Clause)

Adds a clause to this instance.

§Arguments

clause - The clause to add

§Note

If the instance has weights, the new clause gets weight 1.0.

Source

pub fn add_weighted_clause(&mut self, clause: Clause, weight: f64)

Adds a weighted clause to this instance.

If the instance doesn’t have weights yet, this initializes weights with 1.0 for all existing clauses.

§Arguments

clause - The clause to add
weight - The weight for this clause

Source

pub fn num_clauses(&self) -> usize

Returns the number of clauses in this instance.

Source

pub fn is_satisfied(&self, assignment: &[bool]) -> bool

Checks if all clauses are satisfied by the given assignment.

§Arguments

assignment - A slice of boolean values, one per variable

§Returns

true if all clauses are satisfied, false otherwise.

§Example

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

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

assert!(instance.is_satisfied(&[true, true]));
assert!(!instance.is_satisfied(&[true, false]));