Struct Literal 

pub struct Literal {
    pub var: u32,
    pub negated: bool,
}

A propositional variable with optional negation.

Literals are the atomic units of SAT formulas. A literal is either a variable (positive literal) or the negation of a variable (negative literal).

Variables are 0-indexed internally but convert to 1-indexed for DIMACS format.

Memory Layout

The struct is designed for efficient GPU transfer with a compact representation:

• var: 4 bytes (u32 variable index)
• negated: 1 byte (bool), with potential padding

For bulk GPU operations, consider using the packed representation via to_packed().

Fields

var: u32

The variable index (0-indexed).

negated: bool

Whether this literal is negated.

Implementations

impl Literal

pub const fn positive(var: u32) -> Self

Creates a positive literal (variable without negation).

Arguments

• var - The variable index (0-indexed)

Example

use xlog_solve::Literal;
let lit = Literal::positive(3);
assert_eq!(lit.var, 3);
assert!(!lit.negated);

pub const fn negative(var: u32) -> Self

Creates a negative literal (negated variable).

Arguments

• var - The variable index (0-indexed)

Example

use xlog_solve::Literal;
let lit = Literal::negative(3);
assert_eq!(lit.var, 3);
assert!(lit.negated);

pub const fn new(var: u32, negated: bool) -> Self

Creates a literal from a variable and sign.

Arguments

• var - The variable index (0-indexed)
• negated - Whether the literal is negated

pub const fn negate(self) -> Self

Returns the negation of this literal.

Example

use xlog_solve::Literal;
let pos = Literal::positive(5);
let neg = pos.negate();
assert!(neg.negated);
assert_eq!(neg.var, 5);

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

Evaluates this literal under a given assignment.

Arguments

• assignment - A slice of boolean values where index i represents variable i

Returns

true if the literal is satisfied by the assignment, false otherwise.

Panics

Panics if self.var >= assignment.len() (variable index out of bounds).

Example

use xlog_solve::Literal;
let lit = Literal::positive(1);
assert!(lit.eval(&[false, true, false]));  // x1 = true

pub fn to_dimacs(self) -> i32

Converts this literal to DIMACS format.

DIMACS format uses 1-indexed variables, with negative numbers for negated literals.

Returns

A signed integer where:

• Positive values represent positive literals (var + 1)
• Negative values represent negative literals (-(var + 1))

Example

use xlog_solve::Literal;
assert_eq!(Literal::positive(0).to_dimacs(), 1);
assert_eq!(Literal::negative(2).to_dimacs(), -3);

pub fn from_dimacs(dimacs: i32) -> Self

Creates a literal from DIMACS format.

DIMACS format uses 1-indexed variables, with negative numbers for negated literals.

Arguments

• dimacs - A non-zero signed integer in DIMACS format

Panics

Panics if dimacs == 0 (zero is not a valid DIMACS literal).

Example

use xlog_solve::Literal;
let pos = Literal::from_dimacs(3);
assert_eq!(pos.var, 2);
assert!(!pos.negated);

let neg = Literal::from_dimacs(-5);
assert_eq!(neg.var, 4);
assert!(neg.negated);

pub fn to_packed(self) -> u32

Returns a packed 32-bit representation suitable for GPU transfer.

The packed format stores the variable in the lower 31 bits and the negation flag in the most significant bit.

Returns

A u32 where bit 31 is the negation flag and bits 0-30 are the variable.

pub fn from_packed(packed: u32) -> Self

Creates a literal from a packed 32-bit representation.

Arguments

• packed - A u32 with negation in bit 31 and variable in bits 0-30

Trait Implementations

impl Clone for Literal

fn clone(&self) -> Literal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Literal

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

Formats the value using the given formatter.

impl FromIterator<Literal> for Clause

fn from_iter<I: IntoIterator<Item = Literal>>(iter: I) -> Self

Creates a value from an iterator.

impl Hash for Literal

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Literal

fn cmp(&self, other: &Self) -> Ordering

Orders literals first by variable index, then by negation (positive before negative).

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for Literal

fn eq(&self, other: &Literal) -> 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 PartialOrd for Literal

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for Literal

impl Eq for Literal

impl StructuralPartialEq for Literal