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, 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]],
).unwrap();

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

Implementations

impl NonTautology

pub fn new( num_vars: usize, disjuncts: Vec<Vec<i64>>, ) -> Result<Self, ConstructionError>

Create a new Non-Tautology problem.

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<i64>]

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 BruteForceProblem for NonTautology

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

Cardinality of each coordinate in the brute-force search space.

fn num_variables(&self) -> usize

Number of coordinates in the brute-force search space.

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 DeclaredVariant for NonTautology

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 Solution = Vec<bool>

Mathematical witness type for this problem.

type Value = Or

The evaluation value type.

fn parameter_names() -> &'static [&'static str]

Canonical parameter names for this problem model.

fn parameters(&self) -> ProblemParameters

Measure the complete canonical parameters of this concrete instance.

fn evaluate(&self, config: &Self::Solution) -> Result<Or, EvaluationError>

Evaluate the problem on a solution.

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

Returns variant attributes derived from type parameters.

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) -> Result<Self::Result, ReductionError>

Reduce this problem to the target problem type.

fn target_construction(error: ConstructionError) -> ReductionError

where Self: Sized,

Attach this reduction edge to a target-construction failure.

fn exact_i64( value: usize, operation: impl Into<String>, ) -> Result<i64, ReductionError>

where Self: Sized,

Convert a structural count used by the target’s exact integer algebra.

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.