Struct Clause 

pub struct Clause {
    pub literals: Vec<Literal>,
}

A clause is a disjunction (OR) of literals.

In CNF (Conjunctive Normal Form), a formula is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals.

Properties

• An empty clause is always unsatisfied (represents false)
• A clause is satisfied if at least one of its literals is satisfied
• Unit clauses (single literal) are important for unit propagation

Memory Layout

The clause stores literals in a Vec which allows efficient iteration and provides good cache locality for clause evaluation.

Fields

literals: Vec<Literal>

The literals in this clause.

Implementations

impl Clause

pub fn new(literals: Vec<Literal>) -> Self

Creates a new clause from a vector of literals.

Arguments

• literals - The literals forming this disjunction

Example

use xlog_solve::{Clause, Literal};
// Create clause: (x0 OR NOT x1)
let clause = Clause::new(vec![
    Literal::positive(0),
    Literal::negative(1),
]);

pub fn unit(literal: Literal) -> Self

Creates a unit clause (single literal).

Unit clauses are important in SAT solving for unit propagation.

Arguments

• literal - The single literal in this clause

pub fn binary(a: Literal, b: Literal) -> Self

Creates a binary clause (two literals).

Binary clauses are common in many SAT encodings (implications, at-most-one, etc.).

Arguments

• a - The first literal
• b - The second literal

pub fn ternary(a: Literal, b: Literal, c: Literal) -> Self

Creates a ternary clause (three literals).

Arguments

• a - The first literal
• b - The second literal
• c - The third literal

pub fn len(&self) -> usize

Returns the number of literals in this clause.

pub fn is_empty(&self) -> bool

Returns true if this clause has no literals.

An empty clause is always unsatisfied.

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

Checks if this clause is satisfied by the given assignment.

A clause is satisfied if at least one of its literals evaluates to true. An empty clause is never satisfied.

Arguments

• assignment - A slice of boolean values for each variable

Returns

true if the clause is satisfied, false otherwise.

Example

use xlog_solve::{Clause, Literal};
let clause = Clause::new(vec![
    Literal::positive(0),
    Literal::negative(1),
]);
assert!(clause.is_satisfied(&[true, true]));  // x0=true satisfies
assert!(!clause.is_satisfied(&[false, true])); // neither satisfied

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

Counts how many literals in this clause are satisfied by the assignment.

This is useful for CLS solvers and MaxSAT evaluation.

Arguments

• assignment - A slice of boolean values for each variable

Returns

The number of literals that evaluate to true.

pub fn iter(&self) -> impl Iterator<Item = &Literal>

Returns an iterator over the literals in this clause.

pub fn vars(&self) -> impl Iterator<Item = u32> + '_

Returns an iterator over the variable indices in this clause.

Trait Implementations

impl Clone for Clause

fn clone(&self) -> Clause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Clause

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

Formats the value using the given formatter.

impl Eq for Clause

impl FromIterator<Literal> for Clause

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

Creates a value from an iterator.

impl Hash for Clause

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 IntoIterator for Clause

type Item = Literal

The type of the elements being iterated over.

type IntoIter = IntoIter<Literal>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl<'a> IntoIterator for &'a Clause

type Item = &'a Literal

The type of the elements being iterated over.

type IntoIter = Iter<'a, Literal>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Clause

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