RustSAT

https://docs.rs/rustsat
Admin
RustSAT is a comprehensive collection of interfaces and utilities for working with the boolean...
Tokens:622,961
Snippets:3,717
Trust Score:9.1
Update:6 months ago
Show doc for...
Tokens:
Raw
### Example Usage of Documented Item

Source: https://docs.rs/rustsat/latest/scrape-examples-help.html

An example file demonstrating how to call a documented function from another crate. This code will be included in the documentation for `a_func`.

```rust
// examples/ex.rs
fn main() {
  a_crate::a_func();
}
```

--------------------------------

### Main Function Example

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.MultiOptInstance.html

Example of how to use the Rustsat library in a main function, including argument parsing, instance decomposition, conversion, and writing to OPB format.

```APIDOC
## Main Function Example

### Description
This example demonstrates a typical workflow using the Rustsat library. It parses command-line arguments, reads a DIMACS optimization instance (either from a file or stdin), decomposes it, converts soft clauses to hard clauses, composes the instance, and writes the result to an OPB file or stdout.

### Method
N/A (This is a standalone executable example)

### Endpoint
N/A

### Parameters
#### Command Line Arguments (Implicit)
- **first_var_idx** (integer) - Optional - The index of the first variable.
- **avoid_negated_lits** (boolean) - Optional - Whether to avoid negated literals.
- **in_path** (string) - Optional - Path to the input DIMACS file. If not provided, stdin is used.
- **out_path** (string) - Optional - Path to the output OPB file. If not provided, stdout is used.

### Request Example
```bash
./your_program --in_path input.dimacs --out_path output.opb
```

### Response
#### Success Response (0)
- The program exits successfully with status code 0 upon completion.

#### Response Example
(No direct response body, output is written to file or stdout)

### Errors
- `anyhow::Result<()>` indicates potential errors during execution, such as file parsing or writing issues.
```

--------------------------------

### Solve Example: Basic Usage

Source: https://docs.rs/rustsat/latest/rustsat/solvers/trait.Solve.html

Demonstrates how to use a SAT solver by adding a unit clause and solving. This example uses the minisat solver.

```rust
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_unit(lit![0]).unwrap();
let res = solver.solve().unwrap();
debug_assert_eq!(res, SolverResult::Sat);
```

--------------------------------

### wcnf2opb Example

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Example demonstrating the conversion of a WCNF (Weighted Cardinality) file to OPB (Optimized Product Bipartition) format using RustSAT.

```APIDOC
## wcnf2opb Conversion

### Description
Converts a WCNF file to OPB format. It handles input from files or stdin and outputs to files or stdout.

### Method
N/A (Command-line tool)

### Endpoint
N/A (Command-line tool)

### Parameters
#### Command-line Arguments
- **in_path** (Option<PathBuf>) - Optional - Path to the input WCNF file. If not provided, reads from stdin.
- **out_path** (Option<PathBuf>) - Optional - Path to the output OPB file. If not provided, writes to stdout.
- **first_var_idx** (usize) - Optional - The index of the first variable to use.
- **avoid_negated_lits** (bool) - Optional - Whether to avoid negated literals in the output.

### Request Example
```bash
./wcnf2opb --in_path input.wcnf --out_path output.opb
```

### Response
N/A (Writes to file or stdout)

#### Success Response (200)
N/A

#### Response Example
N/A
```

--------------------------------

### mcnf2opb Example

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Example demonstrating the conversion of a multi-objective CNF (MCNF) file to OPB format using RustSAT.

```APIDOC
## mcnf2opb Conversion

### Description
Converts a multi-objective CNF (MCNF) file to OPB format. It supports reading from files or stdin and writing to files or stdout.

### Method
N/A (Command-line tool)

### Endpoint
N/A (Command-line tool)

### Parameters
#### Command-line Arguments
- **in_path** (Option<PathBuf>) - Optional - Path to the input MCNF file. Reads from stdin if not provided.
- **out_path** (Option<PathBuf>) - Optional - Path to the output OPB file. Writes to stdout if not provided.
- **first_var_idx** (usize) - Optional - The index of the first variable.
- **avoid_negated_lits** (bool) - Optional - Flag to avoid negated literals.

### Request Example
```bash
./mcnf2opb --in_path input.mcnf --out_path output.opb
```

### Response
N/A (Writes to file or stdout)

#### Success Response (200)
N/A

#### Response Example
N/A
```

--------------------------------

### Example Usage in build_full_ub

Source: https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html

This example demonstrates how to use `Lit` and `Var` within the `build_full_ub` function, likely for constructing a clause or encoding a problem. It calculates the maximum variable index from a list of literals.

```rust
68fn build_full_ub<PBE: BoundUpper + FromIterator<(Lit, usize)>>(lits: &[(Lit, usize)]) {
    let mut enc = PBE::from_iter(lits.iter().copied());
    let max_var = lits
        .iter()
        .fold(Var::new(0), |mv, (lit, _)| std::cmp::max(lit.var(), mv));
    let mut var_manager = BasicVarManager::default();
    var_manager.increase_next_free(max_var + 1);
    let mut collector = Cnf::new();
    enc.encode_ub(.., &mut collector, &mut var_manager).unwrap();
}
```

--------------------------------

### Solve Example: Get Literal Value

Source: https://docs.rs/rustsat/latest/rustsat/solvers/trait.Solve.html

Shows how to retrieve the assigned value of a literal after solving. This example uses the minisat solver.

```rust
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_unit(lit![0]).unwrap();
let res = solver.solve().unwrap();
debug_assert_eq!(solver.lit_val(lit![0]).unwrap(), TernaryVal::True);
```

--------------------------------

### gbmosplit Example

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Example demonstrating the splitting of a multi-objective Boolean optimization problem (GBM) into multiple single-objective problems.

```APIDOC
## gbmosplit Functionality

### Description
This functionality splits a multi-objective Boolean optimization problem (GBM) into multiple single-objective problems. It can output the results in MCNF or OPB format.

### Method
N/A (Command-line tool)

### Endpoint
N/A (Command-line tool)

### Parameters
#### Command-line Arguments
- **in_path** (Option<PathBuf>) - Optional - Path to the input file. Reads from stdin if not provided.
- **input_format** (InputFormat) - Optional - The format of the input file.
- **opb_opts** (OpbOptions) - Optional - Options for writing OPB format.
- **output_format** (OutputFormat) - Optional - The desired output format (MCNF or OPB).
- **out_path** (Option<PathBuf>) - Optional - Path to the output file. Writes to stdout if not provided.
- **always_dump** (bool) - Optional - Whether to always dump the output even if no split occurs.

### Request Example
```bash
./gbmosplit --in_path input.gbm --output_format OPB --out_path output.opb
```

### Response
N/A (Writes to file or stdout, or exits with status code)

#### Success Response (200)
N/A

#### Response Example
N/A
```

--------------------------------

### Convert OPB to MCNF

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Example demonstrating the conversion of a multi-objective optimization instance to MCNF format.

```rust
fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: 0,
        ..Default::default()
    };

    let inst: MultiOptInstance = if let Some(in_path) = args.in_path {
        MultiOptInstance::from_opb_path(in_path, opb_opts)
            .context("error parsing the input file")?
    } else {
        MultiOptInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
            .context("error parsing input")?
    };

    let (constrs, objs) = inst.decompose();
    let constrs = constrs.sanitize();

    println!("c {} clauses", constrs.n_clauses());
    println!("c {} cards", constrs.n_cards());
    println!("c {} pbs", constrs.n_pbs());
    println!("c {} objectives", objs.len());

    let mut inst = MultiOptInstance::compose(constrs, objs);
    inst.constraints_mut().convert_to_cnf();

    if let Some(out_path) = args.out_path {
        inst.write_dimacs_path(out_path)
            .context("error writing the output file")?;
    } else {
        inst.write_dimacs(&mut io::stdout())
            .context("error writing to stdout")?;
    }
    Ok(())
}
```

--------------------------------

### Main Execution Flow

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.MultiOptInstance.html

Initializes the CLI, parses the instance, performs splitting, and handles output formatting.

```rust
fn main() -> anyhow::Result<()> {
    let cli = Cli::init();

    if let Some(path) = &cli.in_path {
        cli.info(&format!("finding splits in {}", path.display()));
    }

    let (so_inst, write_format) = handle_error!(
        parse_instance(&cli.in_path, cli.input_format, cli.opb_opts),
        cli
    );

    let (mut mo_inst, split_stats) = split(so_inst, &cli);

    if cli.out_path.is_some() {
        cli.print_split_stats(split_stats);
    }

    let found_split = mo_inst.n_objectives() > 1;

    let write_format = cli.output_format.infer(write_format);

    if found_split || cli.always_dump {
        match write_format {
            WriteFormat::Mcnf => {
                mo_inst.constraints_mut().convert_to_cnf();
                if let Some(path) = &cli.out_path {
                    cli.info(&format!("writing mcnf to {}", path.display()));
                    handle_error!(mo_inst.write_dimacs_path(path), cli);
                } else {
                    handle_error(
```

--------------------------------

### Get Variable from Literal

Source: https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html

Gets the `Var` struct that the literal corresponds to. Includes an example demonstrating its usage.

```rust
pub fn var(self) -> Var
```

--------------------------------

### Get Mutable Variable Manager

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Gets a mutable reference to the variable manager.

```APIDOC
## GET /api/variable_manager/mutable

### Description
Gets a mutable reference to the variable manager.

### Method
GET

### Endpoint
/api/variable_manager/mutable

### Response
#### Success Response (200)
- **vm** (VM) - The mutable variable manager.

#### Response Example
```json
{
  "vm": {"num_vars": 10}
}
```
```

--------------------------------

### Get CNF

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Gets a reference to the internal CNF (Conjunctive Normal Form).

```APIDOC
## GET /api/cnf

### Description
Gets a reference to the internal CNF (Conjunctive Normal Form).

### Method
GET

### Endpoint
/api/cnf

### Response
#### Success Response (200)
- **cnf** (Cnf) - The CNF structure.

#### Response Example
```json
{
  "cnf": {"clauses": [[{"var": 1, "neg": false}]]}
}
```
```

--------------------------------

### MultiOptInstance Constructor Methods

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.MultiOptInstance.html

Methods for initializing a new multi-objective optimization instance.

```APIDOC
## new_with_manager

### Description
Creates a new optimization instance with a specific variable manager.

### Parameters
- **n_objs** (usize) - Required - Number of objectives
- **var_manager** (VM) - Required - Variable manager instance

## compose

### Description
Creates a new optimization instance from existing constraints and objectives.

### Parameters
- **constraints** (SatInstance<VM>) - Required - The SAT constraints
- **objectives** (Vec<Objective>) - Required - A list of objectives
```

--------------------------------

### Get Variable Index (u32)

Source: https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html

Gets the 32-bit variable index of the literal.

```rust
pub fn vidx32(self) -> u32
```

--------------------------------

### Initialize External Solver with Custom I/O

Source: https://docs.rs/rustsat/latest/rustsat/solvers/external/struct.Solver.html

Use this to initialize a solver with a custom command, specifying how input is provided and output is received. Input can be via temporary files or direct arguments, and output can be piped or file-based. Note that file-based output does not support compression.

```rust
use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};
let solver = ExternalSolver::new(
    Command::new("<path to solver binary>"),
    external::InputVia::tempfile_last(),
    external::OutputVia::pipe(),
    "solver-signature",
);
```

--------------------------------

### Get Variable Index (usize)

Source: https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html

Gets the variable index of the literal as a `usize`.

```rust
pub fn vidx(self) -> usize
```

--------------------------------

### Initialize OutputVia methods

Source: https://docs.rs/rustsat/latest/rustsat/solvers/external/struct.OutputVia.html

Methods to specify whether solver output is read from a file or a pipe.

```rust
pub fn file<P: AsRef<Path>>(path: P) -> Self
```

```rust
pub fn pipe() -> Self
```

--------------------------------

### Get Literal Value

Source: https://docs.rs/rustsat/latest/src/rustsat/solvers.rs.html

Gets the assignment value (True, False, or Undefined) for a specific literal.

```APIDOC
## GET /solver/lit_val

### Description
Gets an assignment of a literal in the solver.

### Method
GET

### Endpoint
/solver/lit_val

### Parameters
#### Query Parameters
- **lit** (Lit) - Required - The literal to query.

### Response
#### Success Response (200)
- **value** (TernaryVal) - The assignment value of the literal (True, False, or Undefined).

### Errors
- If the solver is not in the satisfied state return [`StateError`]
- A specific implementation might return other errors.
```

--------------------------------

### ExternalSolver::new

Source: https://docs.rs/rustsat/latest/src/rustsat/solvers/external.rs.html

Initializes an external solver with a fully configured command. Input can be provided via files or pipes, and output is processed via pipes.

```APIDOC
## POST /api/users

### Description
Initializes an external solver with a [`Command`] that is fully set up, except for the input instance.

### Method
POST

### Endpoint
/api/users

### Parameters
#### Path Parameters
- **userId** (string) - Required - The ID of the user to retrieve.

#### Query Parameters
- **includeDetails** (boolean) - Optional - Whether to include detailed user information.

#### Request Body
- **username** (string) - Required - The username for the new user.
- **email** (string) - Required - The email address for the new user.

### Request Example
```json
{
  "username": "johndoe",
  "email": "john.doe@example.com"
}
```

### Response
#### Success Response (200)
- **id** (string) - The unique identifier of the created user.
- **username** (string) - The username of the created user.
- **email** (string) - The email address of the created user.

#### Response Example
```json
{
  "id": "123e4567-e89b-12d3-a456-426614174000",
  "username": "johndoe",
  "email": "john.doe@example.com"
}
```
```

--------------------------------

### Get Variable Value

Source: https://docs.rs/rustsat/latest/src/rustsat/solvers.rs.html

Gets the assignment value (True, False, or Undefined) for a specific variable.

```APIDOC
## GET /solver/var_val

### Description
Same as [`Solve::lit_val`], but for variables.

### Method
GET

### Endpoint
/solver/var_val

### Parameters
#### Query Parameters
- **var** (Var) - Required - The variable to query.

### Response
#### Success Response (200)
- **value** (TernaryVal) - The assignment value of the variable (True, False, or Undefined).

### Errors
- If the solver is not in the satisfied state, returns [`StateError`]
- A specific implementation might return other errors.
```

--------------------------------

### Compose and Write Optimization Instance

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.OptInstance.html

Demonstrates creating an OptInstance from parsed input, decomposing it, and writing the result to an OPB file.

```rust
fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: args.first_var_idx,
        no_negated_lits: args.avoid_negated_lits,
    };

    let inst: OptInstance = if let Some(in_path) = args.in_path {
        OptInstance::from_dimacs_path(in_path).context("error parsing the input file")?
    } else {
        OptInstance::from_dimacs(&mut io::BufReader::new(io::stdin()))
            .context("error parsing input")?
    };

    let (mut constr, mut obj) = inst.decompose();
    let hardened = obj.convert_to_soft_lits(constr.var_manager_mut());
    constr.extend(hardened.into());
    let inst = OptInstance::compose(constr, obj);

    if let Some(out_path) = args.out_path {
        inst.write_opb_path(out_path, opb_opts)
            .context("error writing the output file")?;
    } else {
        inst.write_opb(&mut io::stdout(), opb_opts)
            .context("io error writing to stdout")?;
    };
    Ok(())
}
```

--------------------------------

### Start Output Block

Source: https://docs.rs/rustsat/latest/src/gbmosplit/gbmosplit.rs.html

Writes a '>>>>>' marker to denote the start of an output block, with dimmed color.

```rust
buffer.set_color(ColorSpec::new().set_dimmed(true)).unwrap();
        write!(buffer, ">>>>>").unwrap();
        buffer.reset().unwrap();
        writeln!(buffer).unwrap();
```

--------------------------------

### Get Literal Index for Data Structures

Source: https://docs.rs/rustsat/latest/rustsat/types/struct.Lit.html

Gets a literal representation suitable for indexing data structures.

```rust
pub fn lidx(self) -> usize
```

--------------------------------

### Get Literal by Value

Source: https://docs.rs/rustsat/latest/src/rustsat/encodings/totdb.rs.html

Provides a panic-safe way to get a reference to a literal by its value. It internally uses `lit_data_ref`.

```rust
pub fn lit(&self, val: usize) -> Option<&Lit> {
        self.lit_data_ref(val).and_then(LitData::lit)
    }
```

--------------------------------

### Get Database Size

Source: https://docs.rs/rustsat/latest/rustsat/encodings/nodedb/trait.NodeById.html

Gets the total number of nodes currently in the database. This is a required method for the NodeById trait.

```rust
fn len(&self) -> usize;
```

--------------------------------

### BinaryAdder - Trait Implementations

Source: https://docs.rs/rustsat/latest/rustsat/encodings/pb/adder/struct.BinaryAdder.html

Documentation for various trait implementations for BinaryAdder.

```APIDOC
## GET /websites/rs_rustsat/weight_sum

### Description
Get the sum of weights in the encoding.

### Method
GET

### Endpoint
/websites/rs_rustsat/weight_sum

### Response
#### Success Response (200)
- **usize** - The sum of weights.

## GET /websites/rs_rustsat/next_higher

### Description
Gets the next higher value possible to be achieved by the weighted sum. Might simply return `val + 1` if no stronger value can be inferred.

### Method
GET

### Endpoint
/websites/rs_rustsat/next_higher

### Parameters
#### Query Parameters
- **val** (usize) - Required - The current value.

### Response
#### Success Response (200)
- **usize** - The next higher achievable value.

## GET /websites/rs_rustsat/next_lower

### Description
Gets the next lower value possible to be achieved by the weighted sum. Might simply return `val - 1` if no stronger value can be inferred.

### Method
GET

### Endpoint
/websites/rs_rustsat/next_lower

### Parameters
#### Query Parameters
- **val** (usize) - Required - The current value.

### Response
#### Success Response (200)
- **usize** - The next lower achievable value.

## POST /websites/rs_rustsat/reserve

### Description
Reserves all variables this encoding might need.

### Method
POST

### Endpoint
/websites/rs_rustsat/reserve

### Parameters
#### Request Body
- **var_manager** (dyn ManageVars) - Required - The variable manager to use for reserving variables.

### Response
#### Success Response (200)
- **()** - Indicates successful reservation.

## POST /websites/rs_rustsat/fmt

### Description
Formats the value using the given formatter.

### Method
POST

### Endpoint
/websites/rs_rustsat/fmt

### Parameters
#### Request Body
- **f** (Formatter<'_>) - Required - The formatter to use.

### Response
#### Success Response (200)
- **Result** - Ok if formatting is successful, or an error.

## POST /websites/rs_rustsat/default

### Description
Returns the “default value” for a type.

### Method
POST

### Endpoint
/websites/rs_rustsat/default

### Response
#### Success Response (200)
- **BinaryAdder** - The default BinaryAdder instance.

## POST /websites/rs_rustsat/deserialize

### Description
Deserialize this value from the given Serde deserializer.

### Method
POST

### Endpoint
/websites/rs_rustsat/deserialize

### Parameters
#### Request Body
- **__deserializer** (__D) - Required - The Serde deserializer.

### Response
#### Success Response (200)
- **Result<Self, __D::Error>** - The deserialized BinaryAdder instance or an error.

## POST /websites/rs_rustsat/serialize

### Description
Serialize this value into the given Serde serializer.

### Method
POST

### Endpoint
/websites/rs_rustsat/serialize

### Parameters
#### Request Body
- **__serializer** (__S) - Required - The Serde serializer.

### Response
#### Success Response (200)
- **Result<__S::Ok, __S::Error>** - The result of the serialization.
```

--------------------------------

### Creating a New Instance

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.OptInstance.html

Creates a new, empty optimization instance.

```APIDOC
## POST /websites/rs_rustsat/new

### Description
Creates a new optimization instance.

### Method
POST

### Endpoint
`/websites/rs_rustsat/new`

### Response
#### Success Response (200)
- **Instance<VM>** - A new instance object.
```

--------------------------------

### Example Usage of Cardinality Constraints

Source: https://docs.rs/rustsat/latest/src/rustsat/encodings/card.rs.html

Demonstrates how to initialize a variable manager, increase its next free variable, and create a cardinality encoding with upper and lower bounds. Ensure `rustsat` is added as a dependency.

```rust
# use rustsat::{
#     clause,
#     encodings::card::{BoundBoth, DefIncBothBounding, Encode},
#     instances::{BasicVarManager, Cnf, ManageVars},
#     lit,
#     solvers,
#     var,
# };
# 
let mut var_manager = BasicVarManager::default();
var_manager.increase_next_free(var![4]);

let mut enc = DefIncBothBounding::from(vec![lit![0], lit![1], lit![2], lit![3]]);
let mut encoding = Cnf::new();
enc.encode_both(3..=3, &mut encoding, &mut var_manager);

```

--------------------------------

### Convert OPB to CNF

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Example demonstrating how to parse an OPB file into a SatInstance, convert constraints to CNF, and output the result.

```rust
fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: 0,
        ..Default::default()
    };

    let mut inst: SatInstance = if let Some(in_path) = args.in_path {
        SatInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
    } else {
        SatInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
            .context("error parsing input")?
    };

    println!("{} clauses", inst.n_clauses());
    println!("{} cards", inst.n_cards());
    println!("{} pbs", inst.n_pbs());

    inst.convert_to_cnf();

    if let Some(out_path) = args.out_path {
        inst.write_dimacs_path(out_path)
            .context("error writing the output file")?;
    } else {
        inst.write_dimacs(&mut io::stdout())
            .context("error writing to stdout")?;
    }
    Ok(())
}
```

--------------------------------

### Get Connection Literal Count

Source: https://docs.rs/rustsat/latest/rustsat/encodings/nodedb/trait.NodeById.html

Gets the number of literals transmitted by a given NodeCon. This is a provided method in the NodeById trait.

```rust
fn con_len(&self, con: NodeCon) -> usize { ... }
```

--------------------------------

### Convert OPB to WCNF Instance

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.OptInstance.html

Shows how to parse an OPB file into an OptInstance, decompose it, sanitize constraints, and write the result as DIMACS.

```rust
fn main() -> anyhow::Result<()> {
    let args = Args::parse();
    let opb_opts = OpbOptions {
        first_var_idx: 0,
        ..Default::default()
    };

    let inst: OptInstance = if let Some(in_path) = args.in_path {
        OptInstance::from_opb_path(in_path, opb_opts).context("error parsing the input file")?
    } else {
        OptInstance::from_opb(&mut io::BufReader::new(io::stdin()), opb_opts)
            .context("error parsing input")?
    };

    let (constrs, obj) = inst.decompose();
    let mut constrs = constrs.sanitize();

    println!("c {} clauses", constrs.n_clauses());
    println!("c {} cards", constrs.n_cards());
    println!("c {} pbs", constrs.n_pbs());

    constrs.convert_to_cnf();
    let inst = OptInstance::compose(constrs, obj);

    if let Some(out_path) = args.out_path {
        inst.write_dimacs_path(out_path)
            .context("io error writing the output file")?;
    } else {
        inst.write_dimacs(&mut io::stdout())
            .context("io error writing to stdout")?;
    }
    Ok(())
}
```

--------------------------------

### Create and Solve a SAT Instance

Source: https://docs.rs/rustsat/latest/index.html

Demonstrates initializing a SAT instance, adding clauses, and solving it using the Minisat solver interface.

```rust
let mut instance: SatInstance = SatInstance::new();
let l1 = instance.new_lit();
let l2 = instance.new_lit();
instance.add_binary(l1, l2);
instance.add_binary(!l1, l2);
instance.add_unit(l1);
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_cnf(instance.into_cnf().0).unwrap();
let res = solver.solve().unwrap();
assert_eq!(res, SolverResult::Sat);
let sol = solver.full_solution().unwrap();
assert_eq!(sol[l1.var()], TernaryVal::True);
assert_eq!(sol[l2.var()], TernaryVal::True);
```

--------------------------------

### Initialize External Solver with Default I/O

Source: https://docs.rs/rustsat/latest/rustsat/solvers/external/struct.Solver.html

Initializes an external solver using default settings for input and output. Input is handled via a temporary file, and output is processed through a pipe. This is a convenient option when custom I/O configurations are not needed.

```rust
use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};
let solver = ExternalSolver::new_default(
    Command::new("<path to solver binary>"),
    "solver-signature",
);
```

--------------------------------

### Get Core Method

Source: https://docs.rs/rustsat/latest/rustsat/solvers/trait.SolveIncremental.html

Gets a core found by an unsatisfiable query. A core is a clause entailed by the formula that contains only inverted literals of the assumptions. Returns `StateError` if the solver is not in the unsatisfied state.

```rust
fn core(&mut self) -> Result<Vec<Lit>>
```

--------------------------------

### Solver Initialization

Source: https://docs.rs/rustsat/latest/rustsat/solvers/external/struct.Solver.html

Provides details on how to initialize the external Solver struct.

```APIDOC
## Solver Initialization

### Description
Initializes an external SAT solver.

### Methods

#### `new`
```rust
pub fn new( cmd: Command, input: InputVia, output: OutputVia, signature: &'static str, ) -> Self
```

Initializes a solver with a `Command` that is fully set up, except for the input instance.

**Notes:**
* If input is passed via a file with a path that ends in a compression extension, RustSAT will write a compressed file.
* If the solver output is processed via a file, compression is _not_ supported.
* If `Command::env_clear` was called on the command and the input is passed via a file as the first argument, the fact that the environment has been cleared might be forgotten.

**Example:**
```rust
use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};

let solver = ExternalSolver::new(
    Command::new("<path to solver binary>"),
    external::InputVia::tempfile_last(),
    external::OutputVia::pipe(),
    "solver-signature",
);
```

**Hint:**
The only data parsed from the solvers output are the `s` and `v` lines specifying the result and solution. When using a pipe for the solver output, it is therefore recommended to make the solver output as little information as possible (via a `--quiet` flag or similar) to reduce the amount of text RustSAT has to process.

#### `new_default`
```rust
pub fn new_default(cmd: Command, signature: &'static str) -> Self
```

Initializes a solver with default values for `InputVia` and `OutputVia`. The default values are passing the input via a temporary file and processing the output via a pipe.

**Example:**
```rust
use std::process::Command;
use rustsat::solvers::{ExternalSolver, external};

let solver = ExternalSolver::new_default(
    Command::new("<path to solver binary>"),
    "solver-signature",
);
```

**Hint:**
The only data parsed from the solvers output are the `s` and `v` lines specifying the result and solution, it is therefore recommended to make the solver output as little information as possible (via a `--quiet` flag or similar) to reduce the amount of text RustSAT has to process.
```

--------------------------------

### Create New Proof Instance

Source: https://docs.rs/rustsat/latest/src/rustsat/encodings/totdb/cert.rs.html

Initializes a new proof instance using the `pigeons::Proof::new` function. It takes the number of constraints and an optimization flag as parameters.

```rust
fn new_proof(
        num_constraints: usize,
        optimization: bool,
    ) -> pigeons::Proof<tempfile::NamedTempFile> {
        let file = tempfile::NamedTempFile::new().expect("failed to create temporary proof file");
        pigeons::Proof::new(file, num_constraints, optimization).expect("failed to start proof")
    }
```

--------------------------------

### Create Temporary Proof File

Source: https://docs.rs/rustsat/latest/src/rustsat/encodings/pb/gte.rs.html

Initializes a new temporary proof file using the pigeons crate.

```rust
) -> pigeons::Proof<tempfile::NamedTempFile> {
            let file =
                tempfile::NamedTempFile::new().expect("failed to create temporary proof file");
            pigeons::Proof::new(file, num_constraints, optimization).expect("failed to start proof")
        }
```

--------------------------------

### n_clauses

Source: https://docs.rs/rustsat/latest/rustsat/encodings/card/cert/type.DefIncUpperBounding.html

Gets the number of clauses in the encoding.

```APIDOC
## n_clauses

### Description
Retrieves the total number of clauses generated by the encoding.

### Response
- **usize** - The number of clauses.
```

--------------------------------

### Instance Manipulation and I/O

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.MultiOptInstance.html

This section covers the example of shuffling and writing DIMACS files, as well as methods for managing variables and objectives within SAT instances.

```APIDOC
## File Shuffling and Writing

### Description
This example demonstrates how to read a DIMACS file (CNF, WCNF, or MCNF), shuffle its variables using a random re-indexer, and write the modified instance to a new DIMACS file.

### Method
This is an example usage within a `main` function, not a direct API endpoint.

### Endpoint
N/A

### Parameters
- `in_path` (PathBuf) - Required - Path to the input DIMACS file.
- `out_path` (PathBuf) - Required - Path to the output DIMACS file.

### Request Example
```rust
// Example usage within a Rust program:
// let in_path = PathBuf::from(std::env::args().nth(1).unwrap());
// let out_path = PathBuf::from(std::env::args().nth(2).unwrap());
// ... (rest of the logic from shuffledimacs.rs)
```

### Response
- Success: The program completes without errors, and the output file is created.
- Error: Returns an error context if file parsing or writing fails.

### Response Example
N/A (Console output or error messages)

## Variable and Objective Management

### Description
These methods provide functionalities to manage variables and objectives within a SAT instance.

### Method
Various methods associated with SAT instance objects.

### Endpoint
N/A (These are methods on instance objects)

### Parameters
- `obj_idx` (usize) - Required - The index of the objective to access or modify.

### Request Example
```rust
// Example of accessing an objective:
// let objective_ref = instance.objective_ref(0);
// let objective_mut = instance.objective_mut(0);
```

### Response
- `new_var()`: Returns a `Var` representing a newly reserved variable.
- `new_lit()`: Returns a `Lit` representing a newly reserved literal.
- `max_var()`: Returns `Option<Var>` of the highest used variable index.
- `objective_mut(obj_idx)`: Returns a mutable reference to an `Objective`.
- `objective_ref(obj_idx)`: Returns a reference to an `Objective`.
- `iter_obj()`: Returns an iterator over references to objectives.
- `iter_obj_mut()`: Returns an iterator over mutable references to objectives.

### Response Example
```json
// Example response for new_var():
// {"var_index": 5}

// Example response for max_var():
// {"max_var_index": 10}
```

## Instance Conversion and Re-indexing

### Description
Methods for converting instance types and re-indexing variables.

### Method
Various methods associated with SAT instance objects.

### Endpoint
N/A (These are methods on instance objects)

### Parameters
- `reindexer` (R: ReindexVars) - Required - A variable re-indexing manager.
- `vm_converter` (VMC: Fn(&VM) -> VM2) - Required - A function to convert the variable manager.

### Request Example
```rust
// Example of re-indexing:
// let reindexed_instance = instance.reindex(rand_reindexer);

// Example of changing variable manager:
// let converted_instance = instance.change_var_manager(converter_function);
```

### Response
- `into_hard_cls_soft_cls()`: Returns a tuple containing `Cnf`, a vector of soft clauses, and the `VM`.
- `into_hard_cls_soft_lits()`: Returns a tuple containing `Cnf`, a vector of soft literals, and the `VM`.
- `change_var_manager()`: Returns a tuple containing the converted `MultiOptInstance` and the original `VM`.
- `reindex()`: Returns a `MultiOptInstance` with re-indexed variables.

### Response Example
```json
// Example response for into_hard_cls_soft_cls():
// {"cnf": {...}, "soft_clauses": [...], "vm": {...}}
```
```

--------------------------------

### DynamicPolyWatchdogCell::depth

Source: https://docs.rs/rustsat/latest/rustsat/encodings/pb/dpw/referenced/struct.DynamicPolyWatchdogCell.html

Gets the maximum depth of the tree.

```APIDOC
## pub fn depth(&self) -> usize

### Description
Gets the maximum depth of the tree.

### Method
`depth`

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
```rust
// let max_depth = dpw_cell.depth();
```

### Response
#### Success Response (200)
- **usize** - The maximum depth of the tree.

#### Response Example
```rust
// 5 // Example depth value
```
```

--------------------------------

### n_vars

Source: https://docs.rs/rustsat/latest/rustsat/encodings/card/cert/type.DefIncUpperBounding.html

Gets the number of auxiliary variables in the encoding.

```APIDOC
## n_vars

### Description
Retrieves the total number of auxiliary variables used in the encoding.

### Response
- **u32** - The number of variables.
```

--------------------------------

### Initialize CLI Arguments and Options

Source: https://docs.rs/rustsat/latest/src/gbmosplit/gbmosplit.rs.html

Parses command-line arguments and initializes the CLI structure, including input/output paths, formats, splitting algorithm, and color settings for terminal output.

```rust
impl Cli {
    fn init() -> Self {
        let args = Args::parse();
        Self {
            in_path: args.in_path,
            out_path: args.out_path,
            input_format: args.input_format,
            output_format: args.output_format,
            split_alg: args.split_alg,
            max_combs: args.max_combs,
            always_dump: args.always_dump,
            opb_opts: fio::opb::Options {
                first_var_idx: args.opb_first_var_idx,
                ..fio::opb::Options::default()
            },
            stdout: BufferWriter::stdout(match args.color.color {
                concolor_clap::ColorChoice::Always => termcolor::ColorChoice::Always,
                concolor_clap::ColorChoice::Never => termcolor::ColorChoice::Never,
                concolor_clap::ColorChoice::Auto => {
                    if io::stdout().is_terminal() {
                        termcolor::ColorChoice::Auto
                    } else {
                        termcolor::ColorChoice::Never
                    }
                }
            }),
            stderr: BufferWriter::stderr(match args.color.color {
                concolor_clap::ColorChoice::Always => termcolor::ColorChoice::Always,
                concolor_clap::ColorChoice::Never => termcolor::ColorChoice::Never,
                concolor_clap::ColorChoice::Auto => {
                    if io::stderr().is_terminal() {
                        termcolor::ColorChoice::Auto
                    } else {
                        termcolor::ColorChoice::Never
                    }
                }
            }),
        }
    }
}
```

--------------------------------

### Create OutputVia::file

Source: https://docs.rs/rustsat/latest/src/rustsat/solvers/external.rs.html

Constructs an `OutputVia` variant to process solver output by writing it to a specified persistent file. Requires a path for the output file.

```rust
pub fn file<P: AsRef<Path>>(path: P) -> Self {
    OutputVia(OutputViaInt::File(path.as_ref().to_path_buf()))
}
```

--------------------------------

### n_lits

Source: https://docs.rs/rustsat/latest/rustsat/encodings/card/cert/type.DefIncUpperBounding.html

Gets the number of input literals in the encoding.

```APIDOC
## n_lits

### Description
Retrieves the count of input literals currently in the encoding.

### Response
- **usize** - The number of literals.
```

--------------------------------

### Get Subsection

Source: https://docs.rs/rustsat/latest/rustsat/encodings/totdb/struct.AssignIter.html

Returns an iterator over a subsection of the original iterator.

```APIDOC
## fn get<R>(self, index: R) -> <R as IteratorIndex<Self>>::Output

### Description
Returns an iterator over a subsection of the iterator.

### Method
N/A (This is a method on an iterator)

### Endpoint
N/A

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
None

### Response
#### Success Response (200)
An iterator over a subsection of the original iterator.

#### Response Example
None
```

--------------------------------

### Instance::new

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Creates a new, empty satisfiability instance.

```APIDOC
## Instance::new

### Description
Creates a new satisfiability instance.

### Method
`Instance::new()`

### Endpoint
N/A (This is a Rust function, not a web API endpoint)

### Parameters
None

### Request Example
```rust
use rustsat::instance::Instance;

// Assuming VM is a type that implements ManageVars + Default
let instance: Instance<MyVarManager> = Instance::new();
```

### Response
#### Success Response (Instance<VM>)
- **Instance<VM>** - A new instance of the Instance struct.

#### Response Example
```json
// This is a Rust function, not a web API. No JSON response example.
```
```

--------------------------------

### GET /clause_weight

Source: https://docs.rs/rustsat/latest/src/rustsat/instances/opt.rs.html

Retrieves the weight associated with a specific soft clause.

```APIDOC
## GET /clause_weight

### Description
Retrieves the weight of a given soft clause from the objective function.

### Parameters
#### Request Body
- **cl** (Clause) - Required - The clause to query for weight.

### Response
#### Success Response (200)
- **weight** (Option<usize>) - The weight of the clause if it exists.
```

--------------------------------

### into_pbs

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.SatInstance.html

Converts the instance to a set of `PbConstraint`s.

```APIDOC
## into_pbs

### Description
Converts the instance to a set of `PbConstraint`s

### Method
`pub fn into_pbs(self) -> (Vec<PbConstraint>, VM)`
```

--------------------------------

### Get Literal Weight

Source: https://docs.rs/rustsat/latest/src/rustsat/instances/opt.rs.html

Retrieves the current weight of a soft literal.

```APIDOC
## GET /objective/lit_weight

### Description
Gets the weight of a soft literal.

### Method
GET

### Endpoint
/objective/lit_weight

### Parameters
#### Query Parameters
- **l** (Lit) - Required - The literal to query the weight for.

### Request Example
```
GET /objective/lit_weight?l=a
```

### Response
#### Success Response (200)
- **weight** (Option<usize>) - The weight of the literal, if it is present in the objective.
```

--------------------------------

### Parse and Process SAT Instances

Source: https://docs.rs/rustsat/latest/rustsat/instances/struct.OptInstance.html

Example demonstrating how to parse different file formats (CNF, WCNF, MCNF) and perform re-indexing operations.

```rust
124                    let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
125                    MultiOptInstance::compose(inst, vec![obj])
126                } else if is_one_of!(ext, "mcnf") {
127                    MultiOptInstance::from_dimacs_path(inst_path)?
128                } else if is_one_of!(ext, "opb", "mopb", "pbmo") {
129                    MultiOptInstance::from_opb_path(inst_path, opb_opts)?
130                } else {
131                    anyhow::bail!("unknown file extension")
132                };
133                Ok(inst)
134            } else {
135                anyhow::bail!("no file extension")
136            }
137        }
138        FileFormat::Cnf => {
139            let inst = SatInstance::from_dimacs_path(inst_path)?;
140            Ok(MultiOptInstance::compose(inst, vec![]))
141        }
142        FileFormat::Wcnf => {
143            let (inst, obj) = OptInstance::from_dimacs_path(inst_path)?.decompose();
144            Ok(MultiOptInstance::compose(inst, vec![obj]))
145        }
146        FileFormat::Mcnf => MultiOptInstance::from_dimacs_path(inst_path),
147        FileFormat::Opb => MultiOptInstance::from_opb_path(inst_path, opb_opts),
148    }
149}
```

```rust
26fn main() -> anyhow::Result<()> {
27    let in_path = PathBuf::from(&std::env::args().nth(1).unwrap_or_else(|| print_usage!()));
28    let out_path = PathBuf::from(&std::env::args().nth(2).unwrap_or_else(|| print_usage!()));
29
30    match determine_file_type(&in_path) {
31        FileType::Cnf => {
32            let inst = instances::SatInstance::<BasicVarManager>::from_dimacs_path(in_path)
33                .context("Could not parse CNF")?;
34            let n_vars = inst.n_vars();
35            let rand_reindexer = RandReindVarManager::init(n_vars);
36            inst.reindex(rand_reindexer)
37                .shuffle()
38                .write_dimacs_path(out_path)
39                .context("Could not write CNF")?;
40        }
41        FileType::Wcnf => {
42            let inst = instances::OptInstance::<BasicVarManager>::from_dimacs_path(in_path)
43                .context("Could not parse WCNF")?;
44            let n_vars = inst.constraints_ref().n_vars();
45            let rand_reindexer = RandReindVarManager::init(n_vars);
46            inst.reindex(rand_reindexer)
47                .shuffle()
48                .write_dimacs_path(out_path)
49                .context("Could not write WCNF")?;
50        }
51        FileType::Mcnf => {
52            let inst = instances::MultiOptInstance::<BasicVarManager>::from_dimacs_path(in_path)
53                .context("Could not parse MCNF")?;
54            let n_vars = inst.constraints_ref().n_vars();
55            let rand_reindexer = RandReindVarManager::init(n_vars);
56            inst.reindex(rand_reindexer)
57                .shuffle()
58                .write_dimacs_path(out_path)
59                .context("Could not write MCNF")?;
60        }
61    }
62    Ok(())
63}
```

--------------------------------

### Get Variable Set

Source: https://docs.rs/rustsat/latest/src/rustsat/instances/multiopt.rs.html

Retrieves the set of all variables present in the instance.

```APIDOC
## var_set

### Description
Gets the set of all variables currently present in the instance, including those in constraints and objectives.

### Method
`pub fn var_set(&self) -> BTreeSet<Var>`

### Parameters
None

### Request Example
```rust
// Assuming 'instance' is a SatInstance object
let variables = instance.var_set();
```

### Response
- **BTreeSet<Var>** - A set containing all unique variables in the instance.

### Response Example
```json
// Conceptual representation of the returned set
[
  1,
  3,
  5
]
```
```
Tokens:
Raw