problemreductions/models/formula/
mod.rs

1//! Logic and formula problems.
2//!
3//! Problems whose input is a boolean formula or circuit:
4//! - [`Satisfiability`]: Boolean satisfiability (SAT) with CNF clauses
5//! - [`NAESatisfiability`]: Not-All-Equal satisfiability with CNF clauses
6//! - [`KSatisfiability`]: K-SAT where each clause has exactly K literals
7//! - [`Maximum2Satisfiability`]: MAX-2-SAT — maximize satisfied 2-literal clauses
8//! - [`NonTautology`]: Find a falsifying assignment for a DNF formula
9//! - [`OneInThreeSatisfiability`]: Exactly one literal true per clause (1-in-3 SAT)
10//! - [`Planar3Satisfiability`]: 3-SAT restricted to planar variable-clause incidence graphs
11//! - [`CircuitSAT`]: Boolean circuit satisfiability
12//! - [`QuantifiedBooleanFormulas`]: Quantified Boolean Formulas (QBF) — PSPACE-complete
13
14pub(crate) mod circuit;
15pub(crate) mod ksat;
16pub(crate) mod maximum_2_satisfiability;
17pub(crate) mod nae_satisfiability;
18pub(crate) mod non_tautology;
19pub(crate) mod one_in_three_satisfiability;
20pub(crate) mod planar_3_satisfiability;
21pub(crate) mod qbf;
22pub(crate) mod sat;
23
24pub use circuit::{Assignment, BooleanExpr, BooleanOp, Circuit, CircuitSAT};
25pub use ksat::KSatisfiability;
26pub use maximum_2_satisfiability::Maximum2Satisfiability;
27pub use nae_satisfiability::NAESatisfiability;
28pub use non_tautology::NonTautology;
29pub use one_in_three_satisfiability::OneInThreeSatisfiability;
30pub use planar_3_satisfiability::Planar3Satisfiability;
31pub use qbf::{QuantifiedBooleanFormulas, Quantifier};
32pub use sat::{CNFClause, Satisfiability};
33
34#[cfg(feature = "example-db")]
35pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
36    let mut specs = Vec::new();
37    specs.extend(sat::canonical_model_example_specs());
38    specs.extend(nae_satisfiability::canonical_model_example_specs());
39    specs.extend(ksat::canonical_model_example_specs());
40    specs.extend(maximum_2_satisfiability::canonical_model_example_specs());
41    specs.extend(circuit::canonical_model_example_specs());
42    specs.extend(non_tautology::canonical_model_example_specs());
43    specs.extend(one_in_three_satisfiability::canonical_model_example_specs());
44    specs.extend(planar_3_satisfiability::canonical_model_example_specs());
45    specs.extend(qbf::canonical_model_example_specs());
46    specs
47}
problemreductions/models/formula/mod.rs

problemreductions/models/formula/
mod.rs
