cadical-wasm

CaDiCaL — Armin Biere's award-winning SAT solver — compiled to WebAssembly. Works in Node.js and browsers. Built with ALLOW_MEMORY_GROWTH=1, so the heap grows on demand and large instances just work.

• Full incremental (IPASIR-style) API: assumptions, failed() cores, freeze/melt, constraint clauses, phases, options, limits
• Terminate and learned-clause callbacks
• DIMACS CNF parsing helper
• TypeScript declarations included
• Ships as an ES module (cadical.wasm loaded next to the glue code; overridable via locateFile)

Install

npm install cadical-wasm

Quick start

import { Cadical } from 'cadical-wasm';

const solver = await Cadical.create();

// (x1 ∨ x2) ∧ ¬x1
solver.addClause([1, 2]);
solver.addClause([-1]);

console.log(solver.solve());   // 'satisfiable'
console.log(solver.value(1));  // false
console.log(solver.value(2));  // true

solver.dispose(); // optional: frees the native memory immediately
                  // (undisposed solvers are disposed when garbage collected)

One-shot DIMACS solving:

import { solveDimacs } from 'cadical-wasm';

const { status, model } = await solveDimacs(`
p cnf 3 3
1 2 0
-1 3 0
-3 0
`);
// status === 'satisfiable', model[v] is the boolean value of variable v

Incremental solving

const solver = await Cadical.create();
solver.addClause([1, 2]);

solver.solve({ assumptions: [-1, -2] }); // 'unsatisfiable' under these assumptions
solver.failedAssumptions(); // [-1, -2] — an unsatisfiable core

solver.solve();            // 'satisfiable' — assumptions were per-call

Interrupting long solves

solve() runs synchronously on the calling thread. In a browser, run the solver in a Web Worker to keep the UI responsive. To bound or abort a solve:

solver.setTerminate(() => Date.now() > deadline); // poll a deadline, and/or:
solver.solve({ conflicts: 100000 });     // give up after 100k conflicts
                                         // 'unknown' if aborted either way

Learned clauses

solver.setLearn(10, (clause) => {
  // called with each learned clause of length <= 10, e.g. [3, -7]
});

Solver options

CaDiCaL's ~250 options are passed at creation — the solver only accepts them before first use, so making them constructor arguments removes any chance of setting them too late. The SolverOptions type (generated from the pinned CaDiCaL source) documents every option with its default and range, and unknown names throw:

const solver = await Cadical.create({ quiet: true, phase: false });
solver.getOption('phase'); // 0

One option changes the API contract: factor (bounded variable addition, off by default) lets the solver introduce variables of its own, so variable indices become solver-issued. With factor enabled, allocate variables with newVar() or ensureVars() rather than inventing indices — CaDiCaL rejects clause, constraint, and assumption literals with undeclared variables. model() always reports exactly the variables you used or declared, never the solver's internal ones.

Bundlers and the .wasm file

The package ships dist/cadical.js (Emscripten ES-module glue) and dist/cadical.wasm. The glue locates the wasm via import.meta.url, which works out of the box in Node and in bundlers that understand asset URLs (Vite, webpack 5, etc.), so Cadical.create() normally just works.

Module-level settings (locateFile for a custom wasm URL, print/ printErr for output routing) are instantiation-time and shared by every solver on a module, so the shared default module deliberately accepts none. If you need them, create and hold your own module:

import { createModule, Cadical } from 'cadical-wasm';

const mod = await createModule({
  locateFile: (file) => `/static/${file}`, // where cadical.wasm is served
});
const solver = new Cadical(mod);

API

See index.ts for the full typed surface. Highlights:

Method	Description
Cadical.create(options?)	Load the wasm module (cached) and create a solver
addClause(lits) / addClauses(clauses)	Add clauses; literals are non-zero ints (-v negates v)
addDimacs(text)	Stream a DIMACS CNF string into the solver
solve({assumptions?, conflicts?, ...}?)	'satisfiable' | 'unsatisfiable' | 'unknown'; per-call assumptions and limits
value(lit) / model()	Model values after a satisfiable solve
failed(lit) / failedAssumptions()	Unsat core of the assumptions after an unsatisfiable solve
constrain(lits) / constraintFailed()	Constraint clause (see CaDiCaL docs)
setTerminate(cb) / setLearn(max, cb)	Solving callbacks
getOption(name)	Read a solver option's current value
newVar() / ensureVars(maxVar)	Allocate fresh variables / declare unused ones up front
freeze/frozen/melt, phase/unphase, fixed	Advanced incremental controls
simplify(), vars(), active(), irredundant(), printStatistics()	Introspection
dispose() / disposed	Free the native memory now (also via using); GC disposes forgotten solvers eventually

Solvers created with Cadical.create() all share one wasm module (one heap); createModule() makes a fresh, isolated module — useful for a custom locateFile, capturing output, or letting a big solve's memory be reclaimed wholesale when the module is garbage collected:

import { createModule, Cadical } from 'cadical-wasm';
const mod = await createModule();
const a = new Cadical(mod);
const b = new Cadical(mod); // a and b share mod's heap, isolated from the default

Building from source

Requires Emscripten (em++ on PATH), GNU make, git, and npm install (for TypeScript). npm test type-checks the test suite and then runs the .ts test files directly, which needs a Node with type stripping (22.18+ or 24+):

npm run build   # fetches CaDiCaL (pinned tag) into deps/ and builds dist/
npm test

The build pins CaDiCaL rel-3.0.1 (see scripts/fetch-cadical.sh). CaDiCaL's own ./configure cannot cross-compile (it runs test binaries), so scripts/build-wasm.sh instantiates makefile.in directly and links with:

• -O3, ALLOW_MEMORY_GROWTH=1 (16 MB initial heap, grows on demand)
• MODULARIZE + EXPORT_ES6 (factory: createCadicalModule)
• ALLOW_TABLE_GROWTH=1 (for the terminate/learn callbacks)
• ENVIRONMENT=web,webview,worker,node, FILESYSTEM=0

License

MIT for this wrapper. CaDiCaL itself is MIT-licensed (© Armin Biere and contributors) — see its LICENSE.