hub / github.com/c-cube/batsat

github.com/c-cube/batsat @v0.6

Chat with this repo

repository ↗ · DeepWiki ↗ · release v0.6 ↗ · + Follow

483 symbols 1,171 edges 20 files 148 documented · 31%

What it actually does AI analysis from the code graph — generated when you open this

loading…

README

BatSat

This is a Rust SAT solver forked from ratsat, a reimplementation of MiniSat.

For reference, a simple benchmark comparing it to minisat on a set of (easy) problems.

License

MIT licensed.

Features and Goals

Batsat is originally based on ratsat, a clone of minisat. However we want to extend batsat further and to provide the following features:

[x] proof production (in DRAT)
[x] easy access to unsat-cores (as subset of assumptions)
[x] ipasir interface for incremental solving
[ ] testing this interface
[x] debug framework using log (optional)
[x] OCaml bindings
[x] templated API to write SMT solvers
[ ] simplification techniques from Minisat+ (as an optional internal structure)

Extension points exported contracts — how you extend this code

ClauseIterable (Interface)

Anything that can be considered as a list of literals. We use `Into` to have more flexibility for `ClauseRef`, which co [5 …

src/batsat/src/clause.rs

Callbacks (Interface)

Basic callbacks to the solver Typically intended for printing/statistics [5 implementers]

src/batsat/src/callbacks.rs

Theory (Interface)

Theory that parametrizes the solver and can react on events. [2 implementers]

src/batsat/src/theory.rs

DeletePred (Interface)

Predicate that decides whether a value `V` is deleted or not [1 implementers]

src/batsat/src/clause.rs

Print (Interface)

Objects that can be printed in DIMACS syntax [1 implementers]

src/batsat/src/clause.rs

Core symbols most depended-on inside this repo

len

called by 57

src/batsat/src/alloc.rs

var

called by 49

src/batsat/src/clause.rs

iter

called by 20

src/batsat/src/clause.rs

clear

called by 19

src/batsat/src/core.rs

called by 19

src/batsat-sudoku/src/solve.rs

get_ref

called by 18

src/batsat/src/clause.rs

size

called by 17

src/batsat/src/clause.rs

value_lit

called by 15

src/batsat/src/core.rs

Shape

Method 316

Function 87

Class 61

Enum 11

Interface 8

Languages

Rust91%

C9%

Modules by API surface

src/batsat/src/core.rs117 symbols

src/batsat/src/clause.rs91 symbols

src/batsat/src/intmap.rs46 symbols

benchs/drat/drat-trim.c44 symbols

src/batsat/src/callbacks.rs27 symbols

src/batsat-sudoku/src/solve.rs23 symbols

src/batsat-ipasir/src/lib.rs19 symbols

benchs/test_tool/src/main.rs18 symbols

src/batsat/src/alloc.rs17 symbols

src/batsat-bin/src/main.rs17 symbols

src/batsat-sudoku/src/grid.rs15 symbols

src/batsat/src/interface.rs11 symbols

For agents

$ claude mcp add batsat \
  -- python -m otcore.mcp_server <graph>

⬇ download graph artifact