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.