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/// Convert a binary config (0/1 per variable) to a boolean assignment.
35pub(crate) fn config_to_assignment(config: &[usize]) -> Vec<bool> {
36    config.iter().map(|&v| v == 1).collect()
37}
38
39#[cfg(feature = "example-db")]
40pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
41    let mut specs = Vec::new();
42    specs.extend(sat::canonical_model_example_specs());
43    specs.extend(nae_satisfiability::canonical_model_example_specs());
44    specs.extend(ksat::canonical_model_example_specs());
45    specs.extend(maximum_2_satisfiability::canonical_model_example_specs());
46    specs.extend(circuit::canonical_model_example_specs());
47    specs.extend(non_tautology::canonical_model_example_specs());
48    specs.extend(one_in_three_satisfiability::canonical_model_example_specs());
49    specs.extend(planar_3_satisfiability::canonical_model_example_specs());
50    specs.extend(qbf::canonical_model_example_specs());
51    specs
52}
problemreductions/models/formula/mod.rs

problemreductions/models/formula/
mod.rs
