### Cross-Compilation Setup with MinGW32

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Configure CaDiCaL for cross-compilation to a Windows target using MinGW32. This requires Wine to execute binaries on the build host and static linking.

```bash
CXX=i686-w64-mingw32-g++ ./configure -static -lpsapi && make cadical
```

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

### Configure and Build in Release Directory

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Set up a release subdirectory for building and running tests. This ensures the library and binaries in the `release` sub-directory are used.

```bash
mkdir release
cd release
../configure
make test
```

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

### Configure Craig Tracer for Incremental Solving

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/contrib/craigtracer.md

Demonstrates setting up the CaDiCaL solver with a Craig tracer, labeling variables, and applying constraints for interpolation.

```cpp
CaDiCaL::Solver solver;
solver.set ("factor", 0); // important: deactivate BVA
CaDiCraig::CraigTracer tracer;
solver.connect_proof_tracer (&tracer, true);
tracer.set_craig_construction (...);

tracer.label_variable (1, CaDiCraig::CraigVarType::A_LOCAL);
tracer.label_variable (2, CaDiCraig::CraigVarType::GLOBAL);
solver.assume (-1);
solver.assume (2);

tracer.label_constraint (CaDiCraig::CraigClauseType::A_CLAUSE);
solver.constrain (1);
solver.constrain (-2);
solver.constrain (0);

assert (solver.solve () == CaDiCaL::Status::UNSATISFIABLE);
tracer.create_craig_interpolant (...);

solver.disconnect_proof_tracer (&tracer);
```

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

### Handle OPB File I/O

Source: https://context7.com/chrjabs/rustsat/llms.txt

Demonstrates parsing and writing OPB files with custom options for pseudo-boolean constraint problems.

```rust
use rustsat::instances::{SatInstance, ManageVars};
use rustsat::instances::fio::opb;

// Parse OPB file with default options
let instance: SatInstance = SatInstance::from_opb_path(
    "problem.opb",
    opb::Options::default()
).unwrap();

// Parse with custom options
let options = opb::Options {
    first_var_idx: 1,  // OPB uses 1-indexed variables by default
    ..Default::default()
};
let instance2: SatInstance = SatInstance::from_opb_path("problem.opb", options).unwrap();

// Parse from reader
use std::io::BufReader;
let opb_string = "* comment\n+1 x1 +1 x2 >= 1;\n-1 x1 +1 x3 >= 0;\n";
let reader = BufReader::new(std::io::Cursor::new(opb_string));
let instance3: SatInstance = SatInstance::from_opb(reader, opb::Options::default()).unwrap();

// Write to OPB format
let (cnf, vm) = instance.into_cnf();
// instance.write_opb_path("output.opb", opb::Options::default()).unwrap();
```

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

### Manage MaxSAT Optimization Instances

Source: https://context7.com/chrjabs/rustsat/llms.txt

Demonstrates creating optimization instances, adding hard and soft clauses, and parsing/writing WCNF and OPB files.

```rust
use rustsat::instances::{OptInstance, ManageVars};
use rustsat::{lit, clause};

// Create optimization instance
let mut opt_instance: OptInstance = OptInstance::new();

// Add hard clauses (must be satisfied)
opt_instance.add_hard_clause(clause![lit![0], lit![1]]);
opt_instance.add_hard_clause(clause![!lit![2], lit![3]]);

// Add soft clauses with weights (objective to minimize violations)
opt_instance.add_soft_clause(1, clause![lit![0]]);      // Weight 1
opt_instance.add_soft_clause(2, clause![!lit![1]]);     // Weight 2
opt_instance.add_soft_clause(3, clause![lit![2]]);      // Weight 3

// Add soft literals directly to objective
opt_instance.add_soft_lit(1, lit![3]);

// Parse from WCNF file (weighted DIMACS CNF)
let opt_from_file: OptInstance =
    OptInstance::from_dimacs_path("maxsat.wcnf").unwrap();

// Parse from OPB with objective
use rustsat::instances::fio::opb;
let opt_from_opb: OptInstance =
    OptInstance::from_opb_path("optimize.opb", opb::Options::default()).unwrap();

// Get objective information
let obj = opt_instance.objective();
println!("Soft clauses: {}", obj.n_clauses());
println!("Soft literals: {}", obj.n_lits());
println!("Total weight: {}", obj.weight_sum());

// Write to WCNF format
opt_instance.write_dimacs_path("output.wcnf").unwrap();
```

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

### Manual CaDiCaL Build - Application Binaries

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Link the application object files with the static library to create the 'cadical' and 'mobical' executables.

```bash
g++ -o cadical cadical.o -L. -lcadical
g++ -o mobical mobical.o -L. -lcadical
```

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

### Basic SAT Instance and Solver Usage in Rust

Source: https://github.com/chrjabs/rustsat/blob/main/README.md

Demonstrates creating a SAT instance, adding clauses, and solving it using the Minisat solver. Requires `rustsat` and `rustsat-minisat` crates.

```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);
```

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

### Manual CaDiCaL Build - Single Binary

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Compile and link the CaDiCaL solver directly into a single executable without creating a separate library. This is a simplified manual build.

```bash
g++ -O3 -DNDEBUG -DNBUILD -o cadical `ls *.cpp | grep -v mobical`
```

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

### Execute Tests with Make

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Run all tests using the default make goal. Test output is placed in the build directory.

```bash
make test
```

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

### Display Help for Glucose (parallel)

Source: https://github.com/chrjabs/rustsat/blob/main/glucose/vendor/README.md

Displays the help message for the parallel Glucose solver ('glucose-syrup') in the 'parallel' directory. This shows available command-line options for the multicore version.

```bash
./glucose-syrup --help
```

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

### Run Usage Test Driver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Execute a simple usage test for all command line options.

```bash
./usage/run.sh
```

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

### Using IPASIR Interface for Generic SAT Solvers

Source: https://context7.com/chrjabs/rustsat/llms.txt

Demonstrates creating an IPASIR solver, adding clauses, attaching termination and learning callbacks, and solving with assumptions. Requires a linked IPASIR library.

```rust
use rustsat::solvers::{Solve, SolveIncremental, SolverResult, Terminate, Learn, ControlSignal};
use rustsat::types::Clause;
use rustsat::{lit, clause};
use rustsat_ipasir::IpasirSolver;

// Create IPASIR solver (requires linked IPASIR library)
let mut solver = IpasirSolver::default();

// Get solver signature
println!("Solver: {}", solver.signature());

// Add clauses
solver.add_clause(clause![lit![0], lit![1]]).unwrap();
solver.add_clause(clause![!lit![0], lit![2]]).unwrap();

// Attach termination callback
let mut iterations = 0;
solver.attach_terminator(move || {
    iterations += 1;
    if iterations > 1000 {
        ControlSignal::Terminate
    } else {
        ControlSignal::Continue
    }
});

// Attach learner callback to capture learned clauses
solver.attach_learner(|clause: Clause| {
    println!("Learned clause: {}", clause);
}, 10);  // Max clause length to learn

// Solve with assumptions
let result = solver.solve_assumps(&[lit![0]]).unwrap();
match result {
    SolverResult::Sat => println!("SAT"),
    SolverResult::Unsat => {
        let core = solver.core().unwrap();
        println!("UNSAT core: {:?}", core);
    }
    SolverResult::Interrupted => println!("Terminated by callback"),
}

// Detach callbacks when done
solver.detach_terminator();
solver.detach_learner();
```

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

### Configure and build CaDiCaL

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/src/README.md

Executes the configuration script and builds the default optimized version before running the test suite.

```bash
./configure && make test
```

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

### RustSAT SAT Instance Management

Source: https://context7.com/chrjabs/rustsat/llms.txt

Shows how to manage SAT problems using `SatInstance`, including adding clauses, parsing from DIMACS CNF and OPB files, converting to CNF, evaluating assignments, and writing to files. Requires `std::io::BufReader` for file operations.

```rust
use rustsat::instances::{SatInstance, BasicVarManager, ManageVars, Cnf};
use rustsat::types::{Clause, Lit, TernaryVal};
use rustsat::{lit, clause};
use std::io::BufReader;

// Create a new SAT instance
let mut instance: SatInstance = SatInstance::new();

// Add clauses directly
instance.add_clause(clause![lit![0], lit![1]]);       // (x0 ∨ x1)
instance.add_clause(clause![!lit![0], lit![2]]);      // (¬x0 ∨ x2)
instance.add_clause(clause![!lit![1], !lit![2]]);     // (¬x1 ∨ ¬x2)

// Parse from DIMACS CNF file
let instance_from_file: SatInstance = 
    SatInstance::from_dimacs_path("problem.cnf").unwrap();

// Parse from OPB format
use rustsat::instances::fio::opb;
let opb_instance: SatInstance = 
    SatInstance::from_opb_path("problem.opb", opb::Options::default()).unwrap();

// Convert to CNF representation
let (cnf, var_manager) = instance.into_cnf();
println!("CNF has {} clauses", cnf.len());
println!("Maximum variable: {:?}", var_manager.max_var());

// Evaluate an assignment against the instance
use rustsat::types::Assignment;
let assignment = Assignment::from(vec![
    TernaryVal::True,   // x0 = true
    TernaryVal::False,  // x1 = false
    TernaryVal::True,   // x2 = true
]);
let result = instance_from_file.evaluate(&assignment);
match result {
    TernaryVal::True => println!("Assignment satisfies instance"),
    TernaryVal::False => println!("Assignment falsifies instance"),
    TernaryVal::DontCare => println!("Assignment is partial"),
}

// Write instance to file
instance.write_dimacs_path("output.cnf").unwrap();
```

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

### Configure CaDiCaL for Detailed Solver Output

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Include code to observe the solver's internal operations during configuration. This is helpful for understanding solver behavior.

```bash
./configure -l
```

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

### Manual CaDiCaL Build - Library Creation

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Create the static library 'libcadical.a' from the compiled object files, excluding application-specific object files like 'ical.o'.

```bash
ar rc libcadical.a `ls *.o | grep -v ical.o`
```

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

### Display Help for Glucose (simp)

Source: https://github.com/chrjabs/rustsat/blob/main/glucose/vendor/README.md

Displays the help message for the Glucose solver in the 'simp' directory. This shows available command-line options.

```bash
./glucose --help
```

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

### Build Release Version of Glucose

Source: https://github.com/chrjabs/rustsat/blob/main/glucose/vendor/README.md

Builds the release version of the Glucose solver. Navigate to the 'simp' or 'parallel' directory and run 'make rs'.

```bash
cd { simp | parallel }
make rs
```

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

### Solve SAT Instances

Source: https://context7.com/chrjabs/rustsat/llms.txt

A complete workflow for creating a SAT instance, converting it to CNF, solving it, and interpreting the result.

```rust
use rustsat::instances::{SatInstance, ManageVars};
use rustsat::solvers::{Solve, SolveIncremental, SolverResult};
use rustsat::types::TernaryVal;
use rustsat::{lit, clause};
use rustsat_cadical::CaDiCaL;

// Create a SAT instance for the pigeonhole principle (3 pigeons, 2 holes)
// Variables: p_i_j means pigeon i is in hole j
// p_0_0=x0, p_0_1=x1, p_1_0=x2, p_1_1=x3, p_2_0=x4, p_2_1=x5

let mut instance: SatInstance = SatInstance::new();

// Each pigeon must be in at least one hole
instance.add_clause(clause![lit![0], lit![1]]);    // Pigeon 0
instance.add_clause(clause![lit![2], lit![3]]);    // Pigeon 1
instance.add_clause(clause![lit![4], lit![5]]);    // Pigeon 2

// No two pigeons in the same hole
// Hole 0: not (p0 and p1), not (p0 and p2), not (p1 and p2)
instance.add_clause(clause![!lit![0], !lit![2]]); // Not (pigeon 0 and 1 in hole 0)
instance.add_clause(clause![!lit![0], !lit![4]]); // Not (pigeon 0 and 2 in hole 0)
instance.add_clause(clause![!lit![2], !lit![4]]); // Not (pigeon 1 and 2 in hole 0)

// Hole 1
instance.add_clause(clause![!lit![1], !lit![3]]); // Not (pigeon 0 and 1 in hole 1)
instance.add_clause(clause![!lit![1], !lit![5]]); // Not (pigeon 0 and 2 in hole 1)
instance.add_clause(clause![!lit![3], !lit![5]]); // Not (pigeon 1 and 2 in hole 1)

// Convert to CNF and solve
let (cnf, vm) = instance.into_cnf();

let mut solver = CaDiCaL::default();
if let Some(max_var) = vm.max_var() {
    solver.reserve(max_var).unwrap();
}
solver.add_cnf(cnf).unwrap();

match solver.solve().unwrap() {
    SolverResult::Sat => {
        println!("SATISFIABLE - Found assignment:");
        for i in 0..6 {
            let val = solver.lit_val(lit![i]).unwrap();
            let pigeon = i / 2;
            let hole = i % 2;
            if val == TernaryVal::True {
                println!("  Pigeon {} is in hole {}", pigeon, hole);
            }
        }
    }
    SolverResult::Unsat => {
        println!("UNSATISFIABLE - Cannot place 3 pigeons in 2 holes");
        // This is the expected result for pigeonhole principle
    }
    SolverResult::Interrupted => println!("Solving was interrupted"),
}
```

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

### Label Variables and Clauses with CraigTracer

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/contrib/craigtracer.md

Shows how to label variables and clauses using the CraigTracer before adding them to the solver. Variables can be labeled as GLOBAL, A_LOCAL, or B_LOCAL. Clauses can be labeled as A_CLAUSE or B_CLAUSE.

```cpp
CaDiCaL::Solver solver;
solver.set ("factor", 0); // important: deactivate BVA
CaDiCraig::CraigTracer tracer;
solver.connect_proof_tracer (&tracer, true);
tracer.set_craig_construction (CaDiCraig::CraigConstruction::ASYMMETRIC);

tracer.label_variable (1, CaDiCraig::CraigVarType::GLOBAL);
tracer.label_clause (1, CaDiCraig::CraigClauseType::A_CLAUSE);
tracer.label_clause (2, CaDiCraig::CraigClauseType::B_CLAUSE);
solver.add (-1); solver.add (0);
solver.add (1); solver.add (0);
solver.solve ();

solver.disconnect_proof_tracer (&tracer);
```

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

### Attach CraigTracer to CaDiCaL Solver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/contrib/craigtracer.md

Demonstrates how to attach the CraigTracer to a CaDiCaL solver instance and configure the construction type. Ensure 'factor' is set to 0 to deactivate BVA.

```cpp
CaDiCaL::Solver solver;
solver.set ("factor", 0); // important: deactivate BVA
CaDiCraig::CraigTracer tracer;
solver.connect_proof_tracer (&tracer, true);
tracer.set_craig_construction (CaDiCraig::CraigConstruction::ASYMMETRIC);

solver.add (...);
solver.solve ();

solver.disconnect_proof_tracer (&tracer);
```

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

### Run API Test Driver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Execute the simplest test driver that tests basic stand-alone functionality of the library through its API.

```bash
./api/run.sh
```

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

### Link to Custom IPASIR Solver in build.rs

Source: https://github.com/chrjabs/rustsat/blob/main/ipasir/README.md

Configure your build script to link against a custom IPASIR static library. Ensure the library name is provided without the 'lib' prefix and '.a' suffix. Additional flags are required for linking the C++ standard library on macOS and other Unix-like systems.

```rust
println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
println!("cargo:rustc-link-search=<name-of-your-static-lib>");
// If your IPASIR solver links to the C++ stdlib, the next four lines are required
#[cfg(target_os = "macos")]
println!("cargo:rustc-flags=-l dylib=c++");
#[cfg(not(target_os = "macos"))]
println!("cargo:rustc-flags=-l dylib=stdc++\n");
```

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

### Run Traces Test Driver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Execute traces by replaying them through `mobical` using a regression suite.

```bash
./traces/run.sh
```

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

### Enable Proof Logging in CaDiCaL

Source: https://context7.com/chrjabs/rustsat/llms.txt

Configure proof logging for a solver instance before adding clauses. Supported formats include DRAT, LRAT, FRAT, and VeriPB.

```rust
use rustsat::solvers::Solve;
use rustsat::{lit, clause};
use rustsat_cadical::{CaDiCaL, ProofFormat};

let mut solver = CaDiCaL::default();

// Enable proof logging before adding clauses
solver.trace_proof(
    "proof.drat",
    ProofFormat::Drat { binary: false }  // ASCII DRAT format
).unwrap();

// Other proof formats:
// ProofFormat::Drat { binary: true }   // Binary DRAT
// ProofFormat::Lrat { binary: false }  // LRAT (with clause IDs)
// ProofFormat::Frat { binary: false, drat: false }  // FRAT format
// ProofFormat::VeriPB { checked_deletion: true, drat: false }  // VeriPB format

// Add unsatisfiable clauses
solver.add_clause(clause![lit![0]]).unwrap();
solver.add_clause(clause![!lit![0]]).unwrap();

// Solve - proof will be written to file
let result = solver.solve().unwrap();
println!("Result: {:?}", result);  // Unsat
// The proof file can now be verified with DRAT-trim or similar tools
```

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

### Default CaDiCaL Build

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Use this command to configure and build CaDiCaL in the default 'build' sub-directory. This also builds the library libcadical.a and the mobical tester.

```bash
./configure && make
```

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

### RustSAT Core Types and Macros

Source: https://context7.com/chrjabs/rustsat/llms.txt

Demonstrates the creation and usage of fundamental SAT types like variables (Var), literals (Lit), and clauses (Clause) using macros and operators. Includes clause normalization.

```rust
use rustsat::{var, lit, clause};
use rustsat::types::{Var, Lit, Clause};

// Create variables (0-indexed)
let x = var![0];  // Variable x0
let y = var![1];  // Variable x1
let z = var![2];  // Variable x2

// Create literals (positive and negative)
let pos_x = lit![0];     // x0 (positive)
let neg_y = !lit![1];    // ¬x1 (negated)

// Create clauses using the macro
let clause1 = clause![lit![0], !lit![1], lit![2]];  // (x0 ∨ ¬x1 ∨ x2)

// Create clauses using operators
let clause2 = x | !y | z;  // Same clause using variable operators

// Check clause properties
assert_eq!(clause1.len(), 3);
println!("Clause: {}", clause1);  // Prints: 1 -2 3 0

// Normalize clause (sort, deduplicate, check tautology)
let redundant = clause![lit![0], lit![1], lit![0]];
let normalized = redundant.normalize().unwrap();  // Removes duplicate
assert_eq!(normalized.len(), 2);
```

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

### MiniSat Core and Simplified Solver Interfaces

Source: https://context7.com/chrjabs/rustsat/llms.txt

Interface with MiniSat, a classic SAT solver. Use `MinisatCore` for the core solver or `MinisatSimp` with preprocessing. Requires `rustsat-minisat` crate. Freezing variables is important for assumptions with the simplified version.

```rust
use rustsat::solvers::{Solve, SolverResult, FreezeVar};
use rustsat::{lit, clause, var};
use rustsat_minisat::core::Minisat as MinisatCore;
use rustsat_minisat::simp::Minisat as MinisatSimp;

// Use core MiniSat (no preprocessing)
let mut solver = MinisatCore::default();
solver.add_clause(clause![lit![0], lit![1]]).unwrap();
solver.add_clause(clause![!lit![0], lit![1]]).unwrap();

match solver.solve().unwrap() {
    SolverResult::Sat => println!("SAT with core solver"),
    _ => println!("Other result"),
}

// Use MiniSat with simplification/preprocessing
let mut simp_solver = MinisatSimp::default();

// Freeze variables to prevent elimination (important for assumptions)
simp_solver.freeze_var(var![0]).unwrap();
simp_solver.freeze_var(var![1]).unwrap();

simp_solver.add_clause(clause![lit![0], lit![1]]).unwrap();
simp_solver.add_clause(clause![!lit![0], lit![1]]).unwrap();

match simp_solver.solve().unwrap() {
    SolverResult::Sat => {
        let val = simp_solver.lit_val(lit![1]).unwrap();
        println!("x1 = {:?}", val);
    }
    _ => {}
}

```

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

### Totalizer Encoding for Cardinality Constraints

Source: https://context7.com/chrjabs/rustsat/llms.txt

Shows how to use the Totalizer encoding for at-most-k, at-least-k, and exactly-k cardinality constraints. Requires a variable manager and generates CNF clauses.

```rust
use rustsat::encodings::card::{
    BoundUpper, BoundLower, BoundBoth, Encode,
    Totalizer, DefIncBothBounding
};
use rustsat::instances::{BasicVarManager, Cnf, ManageVars};
use rustsat::{lit, var, clause};
use rustsat::types::Lit;

// Create literals for cardinality constraint
let lits: Vec<Lit> = vec![lit![0], lit![1], lit![2], lit![3], lit![4]];

// Initialize variable manager (track next free variable)
let mut var_manager = BasicVarManager::default();
var_manager.increase_next_free(var![5]);  // Variables 0-4 are used

// Create Totalizer encoding for "at most 2 of 5 literals are true"
let mut enc = Totalizer::from_iter(lits.clone());
let mut cnf = Cnf::new();

// Encode upper bound (at-most-k)
enc.encode_ub(0..=2, &mut cnf, &mut var_manager).unwrap();

// Get assumptions to enforce the bound
let assumptions = enc.enforce_ub(2).unwrap();
println!("Assumptions for at-most-2: {:?}", assumptions);
println!("Generated {} clauses", cnf.len());

// For lower bound (at-least-k)
let mut enc_lb = Totalizer::from_iter(lits.clone());
let mut cnf_lb = Cnf::new();
enc_lb.encode_lb(3..=5, &mut cnf_lb, &mut var_manager).unwrap();
let lb_assumptions = enc_lb.enforce_lb(3).unwrap();  // At least 3 true
println!("Assumptions for at-least-3: {:?}", lb_assumptions);

// For equality constraint (exactly-k)
let mut enc_eq = DefIncBothBounding::from_iter(lits);
let mut cnf_eq = Cnf::new();
enc_eq.encode_both(2..=2, &mut cnf_eq, &mut var_manager).unwrap();
let eq_assumptions = enc_eq.enforce_eq(2).unwrap();  // Exactly 2 true
println!("Assumptions for exactly-2: {:?}", eq_assumptions);
```

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

### Manual CaDiCaL Build - Object Compilation

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Manually compile all source files in the 'src' directory into object files. This method bypasses the configure script and GNU make.

```bash
mkdir build
cd build
for f in ../src/*.cpp; do g++ -O3 -DNDEBUG -DNBUILD -c $f; done
```

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

### Kissat Solver Interface

Source: https://context7.com/chrjabs/rustsat/llms.txt

Integrate with the Kissat SAT solver for high-performance solving. Supports retrieving version, signature, and statistics. Requires `rustsat-kissat` crate.

```rust
use rustsat::solvers::{Solve, SolveStats, SolverResult, Terminate, ControlSignal};
use rustsat::{lit, clause};
use rustsat_kissat::Kissat;

// Create Kissat solver
let mut solver = Kissat::default();

// Check solver information
println!("Kissat version: {}", Kissat::version());
println!("Kissat signature: {}", solver.signature());

// Add clauses
solver.add_clause(clause![lit![0], lit![1], lit![2]]).unwrap();
solver.add_clause(clause![!lit![0], !lit![1]]).unwrap();
solver.add_clause(clause![!lit![1], !lit![2]]).unwrap();
solver.add_clause(clause![!lit![0], !lit![2]]).unwrap();

// Solve and get solution
match solver.solve().unwrap() {
    SolverResult::Sat => {
        let solution = solver.full_solution().unwrap();
        println!("Solution found: {}", solution);
    }
    SolverResult::Unsat => println!("No solution exists"),
    SolverResult::Interrupted => println!("Solver was interrupted"),
}

// Get solver statistics
let stats = solver.stats();
println!("Clauses added: {}", stats.n_clauses);
println!("Solve time: {:?}", stats.cpu_solve_time);

```

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

### Configure CaDiCaL for Debugging

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Configure CaDiCaL to include debugging information and detailed solver output. Use this for development and troubleshooting.

```bash
./configure -a
```

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

### Run Model-Based Test Driver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Execute the most effective test driver, the model-based tester `../src/mobical.cpp`.

```bash
./mbt/run.sh
```

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

### Configure Solver Limits and Options

Source: https://context7.com/chrjabs/rustsat/llms.txt

Configures solver behavior using pre-defined settings, custom options, and execution limits like conflict or decision counts.

```rust
use rustsat::solvers::{Solve, LimitConflicts, LimitDecisions, SolverResult};
use rustsat::{lit, clause};
use rustsat_cadical::{CaDiCaL, Config, Limit};

let mut solver = CaDiCaL::default();

// Set pre-defined configuration before adding clauses
solver.set_configuration(Config::Sat).unwrap();  // Optimize for SAT instances
// Other configs: Config::Unsat, Config::Plain, Config::Default

// Set specific options
solver.set_option("restart", 1).unwrap();
solver.set_option("phase", 1).unwrap();

// Get option values
let restart_val = solver.get_option("restart").unwrap();
println!("Restart option: {}", restart_val);

// Add clauses
solver.add_clause(clause![lit![0], lit![1]]).unwrap();
solver.add_clause(clause![!lit![0], lit![2]]).unwrap();

// Set solving limits
solver.set_limit(Limit::Conflicts(10000)).unwrap();    // Max 10000 conflicts
solver.set_limit(Limit::Decisions(50000)).unwrap();    // Max 50000 decisions

// Alternative: use trait methods
solver.limit_conflicts(Some(10000)).unwrap();
solver.limit_decisions(Some(50000)).unwrap();

// Solve with limits
match solver.solve().unwrap() {
    SolverResult::Sat => println!("SAT"),
    SolverResult::Unsat => println!("UNSAT"),
    SolverResult::Interrupted => println!("Limit reached"),
}

// Get solver statistics
println!("Active variables: {}", solver.get_active());
println!("Irredundant clauses: {}", solver.get_irredundant());
println!("Redundant (learned) clauses: {}", solver.get_redundant());
```

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

### Handle DIMACS CNF File I/O

Source: https://context7.com/chrjabs/rustsat/llms.txt

Provides methods for parsing and writing DIMACS CNF files, including support for compressed files and solver output parsing.

```rust
use rustsat::instances::SatInstance;
use rustsat::instances::fio::{self, SolverOutput};
use rustsat::types::Assignment;
use std::io::{BufReader, BufWriter, Cursor};
use std::fs::File;

// Parse DIMACS CNF from file
let instance: SatInstance = SatInstance::from_dimacs_path("problem.cnf").unwrap();

// Parse from string
let cnf_string = "p cnf 3 2\n1 2 0\n-1 3 0\n";
let reader = BufReader::new(Cursor::new(cnf_string));
let instance2: SatInstance = SatInstance::from_dimacs(reader).unwrap();

// Parse compressed files (requires "compression" feature)
let compressed_instance: SatInstance =
    SatInstance::from_dimacs_path("problem.cnf.gz").unwrap();

// Write to DIMACS format
instance.write_dimacs_path("output.cnf").unwrap();

// Write to writer
let mut buffer = Vec::new();
instance.write_dimacs(&mut buffer).unwrap();

// Parse SAT solver output
let solver_output = "c comment\ns SATISFIABLE\nv 1 -2 3 0\n";
let reader = BufReader::new(Cursor::new(solver_output));
match fio::parse_sat_solver_output(reader).unwrap() {
    SolverOutput::Sat(assignment) => {
        println!("Solution: {}", assignment);
    }
    SolverOutput::Unsat => println!("UNSATISFIABLE"),
    SolverOutput::Unknown => println!("UNKNOWN"),
}
```

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

### Encode Pseudo-Boolean Constraints

Source: https://context7.com/chrjabs/rustsat/llms.txt

Demonstrates using Generalized Totalizer, Dynamic Poly Watchdog, and DefIncBothBounding to encode weighted literals into CNF.

```rust
use rustsat::encodings::pb::{
    BoundUpper, BoundLower, BoundBoth, Encode,
    GeneralizedTotalizer, DynamicPolyWatchdog, DefIncBothBounding
};
use rustsat::instances::{BasicVarManager, Cnf, ManageVars};
use rustsat::types::{Lit, RsHashMap};
use rustsat::{lit, var};

// Create weighted literals: 4*x0 + 2*x1 + 2*x2 + 6*x3
let mut weighted_lits: RsHashMap<Lit, usize> = RsHashMap::default();
weighted_lits.insert(lit![0], 4);
weighted_lits.insert(lit![1], 2);
weighted_lits.insert(lit![2], 2);
weighted_lits.insert(lit![3], 6);

let mut var_manager = BasicVarManager::default();
var_manager.increase_next_free(var![4]);

// Use Generalized Totalizer for upper bound
let mut gte = GeneralizedTotalizer::from_iter(weighted_lits.clone());
let mut cnf = Cnf::new();

// Encode: weighted sum <= 8
gte.encode_ub(0..=8, &mut cnf, &mut var_manager).unwrap();
let assumptions = gte.enforce_ub(8).unwrap();
println!("PB encoding generated {} clauses", cnf.len());
println!("Weight sum: {}", gte.weight_sum());

// Use Dynamic Poly Watchdog for incremental solving
let mut dpw = DynamicPolyWatchdog::from_iter(weighted_lits.clone());
let mut cnf_dpw = Cnf::new();
dpw.encode_ub(0..=10, &mut cnf_dpw, &mut var_manager).unwrap();

// Get next coarse bound for efficient search
let coarse = dpw.coarse_ub(7);  // Find efficient bound near 7
println!("Coarse upper bound: {}", coarse);

// For both upper and lower bounds
let mut double_enc = DefIncBothBounding::from(weighted_lits);
let mut cnf_both = Cnf::new();
double_enc.encode_both(4..=10, &mut cnf_both, &mut var_manager).unwrap();
let eq_assumps = double_enc.enforce_eq(6).unwrap();  // Weighted sum = 6
```

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

### Configure CaDiCaL with Assertion Checking

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/BUILD.md

Enable assertion checking code during configuration. This is useful for debugging.

```bash
./configure -c
```

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

### Run CNF Regression Test Driver

Source: https://github.com/chrjabs/rustsat/blob/main/cadical/vendor/test/README.md

Execute the regression suite for CNF files, which is more thorough and checks solutions and generated proofs.

```bash
./cnf/run.sh
```

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

### CaDiCaL Solver Interface

Source: https://context7.com/chrjabs/rustsat/llms.txt

Use this for high-performance CDCL SAT solving with incremental capabilities and assumptions. Requires `rustsat-cadical` crate.

```rust
use rustsat::solvers::{Solve, SolveIncremental, SolverResult};
use rustsat::types::{Lit, TernaryVal};
use rustsat::{lit, clause};
use rustsat_cadical::CaDiCaL;

// Create a new CaDiCaL solver instance
let mut solver = CaDiCaL::default();

// Add clauses to the solver
solver.add_clause(clause![lit![0], lit![1]]).unwrap();      // (x0 ∨ x1)
solver.add_clause(clause![!lit![0], lit![2]]).unwrap();     // (¬x0 ∨ x2)
solver.add_clause(clause![!lit![1], !lit![2]]).unwrap();    // (¬x1 ∨ ¬x2)
solver.add_clause(clause![lit![1], lit![2]]).unwrap();      // (x1 ∨ x2)

// Solve the SAT problem
match solver.solve().unwrap() {
    SolverResult::Sat => {
        println!("SATISFIABLE");
        // Get variable assignments
        let val_x0 = solver.lit_val(lit![0]).unwrap();
        let val_x1 = solver.lit_val(lit![1]).unwrap();
        let val_x2 = solver.lit_val(lit![2]).unwrap();
        println!("x0={:?}, x1={:?}, x2={:?}", val_x0, val_x1, val_x2);

        // Get full solution
        let solution = solver.full_solution().unwrap();
        println!("Full solution: {}", solution);
    }
    SolverResult::Unsat => println!("UNSATISFIABLE"),
    SolverResult::Interrupted => println!("INTERRUPTED"),
}

// Incremental solving with assumptions
let assumps = vec![lit![0], !lit![1]];  // Assume x0=true, x1=false
match solver.solve_assumps(&assumps).unwrap() {
    SolverResult::Unsat => {
        // Get unsatisfiable core
        let core = solver.core().unwrap();
        println!("UNSAT core: {:?}", core);
    }
    _ => {}
}

```