# [−][src]Crate varisat

Varisat is a CDCL based SAT solver written in rust. Given a boolean formula in conjunctive normal form, it either finds a variable assignment that makes the formula true or finds a proof that this is impossible.

In addition to this API documentation, Varisat comes with a user manual.

## Re-exports

`pub use solver::Solver;` |

## Modules

analyze_conflict | Learns a new clause by analyzing a conflict. |

assumptions | Incremental solving. |

binary | Binary clauses. |

cdcl | Conflict driven clause learning. |

checker | Proof checker for Varisat proofs. |

clause | Clause storage. |

cnf | CNF formulas. |

config | Solver configuration. |

context | Central solver data structure. |

decision | Decision heuristics. |

dimacs | DIMCAS CNF parser and writer. |

glue | Compute glue levels of clauses. |

lit | Literals and variables. |

load | Loading a formula into the solver. |

model | Global model reconstruction |

proof | Proof generation. |

prop | Unit propagation. |

schedule | Scheduling of processing and solving steps. |

solver | Boolean satisfiability solver. |

state | Miscellaneous solver state. |

tmp | Temporary data. |

unit_simplify | Simplification using unit clauses. |

variables | Variable mapping and metadata. |

## Macros

cnf | Shortcut for tests |

lit | Shortcut for tests |

## Structs

CnfFormula | A formula in conjunctive normal form (CNF). |

Lit | A boolean literal. |

Var | A boolean variable. |

## Enums

ProofFormat | Proof formats that can be generated during solving. |

## Traits

ExtendFormula | Extend a formula with new variables and clauses. |