rustsat 0.6.4

This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66

//! # CNF Encodings for At-Most-1 Constraints
//!
//! The module contains implementations of CNF encodings for at-most-1
//! constraints.
//!
//! ## Example Usage
//!
//! ```
//! # use rustsat::{
//! #     encodings::am1::{Def, Encode},
//! #     instances::{BasicVarManager, Cnf, ManageVars},
//! #     lit, var,
//! # };
//! #
//! let mut var_manager = BasicVarManager::default();
//! var_manager.increase_next_free(var![3]);
//!
//! let mut enc = Def::from(vec![lit![0], lit![1], lit![2]]);
//! let mut encoding = Cnf::new();
//! enc.encode(&mut encoding, &mut var_manager).unwrap();
//! ```

use super::CollectClauses;
use crate::instances::ManageVars;

mod pairwise;
pub use pairwise::Pairwise;

mod ladder;
pub use ladder::Ladder;

mod bitwise;
pub use bitwise::Bitwise;

mod commander;
pub use commander::Commander;

mod bimander;
pub use bimander::Bimander;

/// Trait for all at-most-1 encodings
pub trait Encode {
    /// Gets the number of literals in the encoding
    fn n_lits(&self) -> usize;
    /// Encodes and enforces the at-most-1 constraint
    ///
    /// # Errors
    ///
    /// If the clause collector runs out of memory, returns [`crate::OutOfMemory`].
    fn encode<Col>(
        &mut self,
        collector: &mut Col,
        var_manager: &mut dyn ManageVars,
    ) -> Result<(), crate::OutOfMemory>
    where
        Col: CollectClauses;
}

/// The default at-most-1 encoding. For now this is a [`Pairwise`] encoding.
pub type Def = Pairwise;

/// Constructs a default at-most-1 encoding.
#[must_use]
pub fn new_default() -> impl Encode {
    Def::default()
}