cadical

A Ruby binding for CaDiCaL, a state-of-the-art incremental SAT solver. The CaDiCaL C++ sources are vendored and compiled straight into the extension, so there is no external dependency.

This is a thin, general-purpose binding over CaDiCaL's C API (ccadical_*). The Ruby class is CaDiCaL, and CaDiCaL.new creates a solver.

Installation

gem install cadical

Building the extension requires a C++17 compiler.

Usage

A literal is an Integer in DIMACS form: positive v = "variable v is true", -v = false. A clause is just a list of literals.

require "cadical"

c = CaDiCaL.new
x1, x2 = c.new_var, c.new_var

c.add(x1, x2)     # (x1 \/ x2)
c.add(x1, -x2)    # (x1 \/ !x2)
c.add(-x1, -x2)   # (!x1 \/ !x2)

c.solve           # => :sat
c.true?(x1)       # => true
c.true?(x2)       # => false

Incremental solving

Clauses added with #add stay for good, so you can keep solving as you learn more. An assumption is a temporary hypothesis for the next #solve only -- handy to pose what-if questions without rebuilding the formula:

c.assume(-x1)     # what if x1 were false?
c.solve           # => :unsat -- the clauses above force x1 true
c.solve           # => :sat again; the assumption is already gone

A constraint is the same idea but a whole clause (a disjunction), at most one at a time:

c.constrain(-x1, x2)    # require (!x1 \/ x2) for the next solve only
c.solve                 # => :unsat
c.constraint_failed?    # => true -- the constraint is what made it unsat

API

CaDiCaL (every ccadical_* function, plus a couple of conveniences)

method	C function	description
`CaDiCaL.signature`	`ccadical_signature`	the bundled CaDiCaL version string
`CaDiCaL.new`	`ccadical_init`	create a solver
`#release`	`ccadical_release`	free the solver now (else at GC)
`#add(*lits)`	`ccadical_add`	add a permanent clause (splat an array: `add(*clause)`)
`#assume(lit)`	`ccadical_assume`	assume a literal for the next `solve` only
`#constrain(*lits)`	`ccadical_constrain`	temporary constraint clause for the next `solve`
`#constraint_failed?`	`ccadical_constraint_failed`	did the constraint cause the last UNSAT?
`#solve`	`ccadical_solve`	solve -> `:sat` / `:unsat` / `:unknown`
`#simplify`	`ccadical_simplify`	inprocessing -> `:sat` / `:unsat` / `:unknown`
`#val(lit)`	`ccadical_val`	raw model value (signed literal)
`#failed(lit)`	`ccadical_failed`	did this assumption take part in the last UNSAT core?
`#fixed(lit)`	`ccadical_fixed`	`1` / `-1` / `0`: proven true / false / not yet fixed
`#set_terminate { }`	`ccadical_set_terminate`	abort `solve` when the block is truthy (no block clears)
`#set_learn(max) { \|clause\| }`	`ccadical_set_learn`	observe learned clauses (no block clears)
`#terminate`	`ccadical_terminate`	force the running solve to stop
`#declare_one_more_variable`	`ccadical_declare_one_more_variable`	allocate one fresh variable
`#declare_more_variables(n)`	`ccadical_declare_more_variables`	allocate `n` variables
`#vars`	`ccadical_vars`	number of variables
`#phase(lit)` / `#unphase(lit)`	`ccadical_phase` / `ccadical_unphase`	set / clear a forced decision phase
`#freeze_lit(lit)` / `#melt_lit(lit)` / `#frozen_lit?(lit)`	`ccadical_freeze` / `_melt` / `_frozen`	freeze a literal against elimination
`#set_option(name, v)` / `#get_option(name)`	`ccadical_set_option` / `_get_option`	options
`#limit(name, v)`	`ccadical_limit`	set a solve limit
`#active` / `#irredundant`	`ccadical_active` / `_irredundant`	active-variable / irredundant-clause counts
`#trace_proof(path)` / `#close_proof` / `#conclude`	`ccadical_trace_proof` / `_close_proof` / `_conclude`	DRAT proof tracing
`#new_var`	--	alias for `#declare_one_more_variable`
`#true?(lit)`	--	convenience boolean: is `lit` assigned true?
`#true_var` / `#false_var`	--	a variable pinned true / false, usable as a constant literal

Notes

Unlike many SAT-solver APIs where any integer can be used as a literal directly, the bundled CaDiCaL (with its defaults) rejects a literal whose variable was not produced by #new_var (the examples above use it). Set c.set_option("factor", 0) to allow raw integer literals.

License

MIT. The bundled CaDiCaL solver (ext/cadical/cadical/) is also MIT-licensed; see ext/cadical/cadical/LICENSE.