cadical

name	cadical
description	Write correct C++ code using the CaDiCaL 3.0.0 SAT solver API. Triggers on: "cadical", "CaDiCaL", "SAT solver", "CDCL", "DIMACS", "CNF", "ExternalPropagator", "external propagator", "IPASIR", "satisfiability", "solver.add", "solver.solve", "solver.val", "cadical.hpp", "#include \"cadical"

CaDiCaL 3.0.0 SAT Solver

CaDiCaL is a C++ CDCL SAT solver. Version 3.0.0 has several API changes from 2.x that commonly trip up developers. This skill provides the reference material to write correct CaDiCaL code.

Quick Start

#include "cadical.hpp"

CaDiCaL::Solver solver;
solver.add(1); solver.add(2); solver.add(0);   // clause: x1 ∨ x2
solver.add(-1); solver.add(-2); solver.add(0);  // clause: ¬x1 ∨ ¬x2
int res = solver.solve();
if (res == 10) {
    int v1 = solver.val(1);  // positive = true, negative = false
}

Before Writing Any CaDiCaL Code

If you run into crashes, wrong results, or confusing behavior, read references/gotchas.md. It covers 33 common pitfalls, many CaDiCaL 3.0.0-specific, that won't match what you know from other SAT solvers.

Reference Selection

Load references based on what the task requires:

If the task involves...	Read this reference
Basic solving, adding clauses, querying models	references/api-basics.md
Multiple solve() calls, incremental solving	references/api-basics.md (incremental section)
Temporary queries, assumption-based probing	references/assumptions.md
constrain() / constraint_failed() (IC3)	references/constraints.md
ExternalPropagator, callbacks, CEGAR	references/external-propagator.md
LRAT/DRAT proof generation	references/proof-tracing.md
Preprocessing, simplify(), options	references/preprocessing.md
Complete list of solver options	references/options-reference.md
Terminator, learner, fixed-listener callbacks	references/api-basics.md (callback section)
Phase control, lookahead, cubes, flip/flippable	references/api-basics.md
DIMACS I/O, solver copying, clause traversal	references/api-basics.md
Debugging crashes or wrong results	references/gotchas.md

Load at most 2-3 references per task. Read gotchas.md plus the most relevant API reference for the task.

Critical Rules (Always Apply)

These are the highest-priority rules. Violating any of these causes crashes or wrong results:

1. Options before clauses: set() only works before the first add() call.
2. val() only after SAT: Calling val() when solve() didn't return 10 crashes.
3. Assumptions are temporary: assume() is consumed by solve(). Use assume() for temporary queries, add() for permanent clauses. Never use add() for temporary constraints.
4. Variable allocation with BVA: CaDiCaL 3.0.0 has BVA enabled by default. Use declare_more_variables(N) to allocate variables safely, or disable BVA with solver.set("factor", 0).
5. Propagator before observation: Call connect_external_propagator() before add_observed_var().
6. Reason clauses include the propagated literal: In cb_add_reason_clause_lit, the clause must contain the literal that was propagated.