Struct NonTautology 

pub struct NonTautology { /* private fields */ }

Non-Tautology problem.

Given a Boolean formula in DNF (disjunctive normal form) with disjuncts D_1, …, D_m, find a truth assignment that makes ALL disjuncts false (i.e., the formula is not a tautology).

A disjunct is a conjunction (AND) of literals. The DNF formula is the disjunction (OR) of all disjuncts. The formula is false when every disjunct is false, which happens when each disjunct has at least one false literal.

Example

use problemreductions::models::formula::NonTautology;
use problemreductions::{Problem, Solver, BruteForce};

// (x1 AND x2 AND x3) OR (NOT x1 AND NOT x2 AND NOT x3)
let problem = NonTautology::new(
    3,
    vec![vec![1, 2, 3], vec![-1, -2, -3]],
);

let solver = BruteForce::new();
let solution = solver.find_witness(&problem);
assert!(solution.is_some());

Implementations

impl NonTautology

pub fn new(num_vars: usize, disjuncts: Vec<Vec<i32>>) -> Self

Create a new Non-Tautology problem.

Panics

Panics if any literal references a variable outside the range [1, num_vars].

pub fn num_vars(&self) -> usize

Get the number of variables.

pub fn num_disjuncts(&self) -> usize

Get the number of disjuncts.

pub fn disjuncts(&self) -> &[Vec<i32>]

Get the disjuncts.

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

Check if all disjuncts are false (the formula evaluates to false).

A disjunct (conjunction of literals) is true iff ALL its literals are true. The DNF formula is false iff ALL disjuncts are false, i.e., each disjunct has at least one false literal.

Trait Implementations

impl Clone for NonTautology

fn clone(&self) -> NonTautology

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NonTautology

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for NonTautology

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Problem for NonTautology

const NAME: &'static str = "NonTautology"

Base name of this problem type (e.g., “MaximumIndependentSet”).

type Value = Or

The evaluation value type.

fn dims(&self) -> Vec<usize>

Configuration space dimensions. Each entry is the cardinality of that variable.

fn evaluate(&self, config: &[usize]) -> Or

Evaluate the problem on a configuration.

fn variant() -> Vec<(&'static str, &'static str)>

Returns variant attributes derived from type parameters.

fn num_variables(&self) -> usize

Number of variables (derived from dims).

fn problem_type() -> ProblemType

Look up this problem’s catalog entry.

impl ReduceTo<NonTautology> for Satisfiability

type Result = ReductionSATToNonTautology

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl Serialize for NonTautology

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl DeclaredVariant for NonTautology