zusat

R bindings for CaDiCaL, a modern CDCL Boolean satisfiability (SAT) solver by Armin Biere and colleagues.

The CaDiCaL sources are bundled, so there is nothing to install beyond the package itself and a C++ compiler.

Installation

install.packages("zusat")

Or the development version from GitHub:

# install.packages("pak")
pak::pak("pedrobtz/zusat")

Solving a formula

Clauses use DIMACS conventions: i means "variable i is true", -i means its negation. No terminating zero is needed.

library(zusat)

# (x1 OR x2) AND (NOT x1 OR x2)
sat_solve(list(c(1, 2), c(-1, 2)))
#> <zusat_solution> sat  (2 variables, 2 active clauses, 0.000s)
#>  variable value
#>         1  TRUE
#>         2  TRUE

A solution is a data frame of variable and value, so it drops straight into the rest of R:

sol <- sat_solve(list(c(1, 2), c(-1, 3)))

sat_status(sol)       #> "sat"
sat_is_sat(sol)       #> TRUE
sat_assignment(sol)   #> named logical vector
subset(sol, value)    #> just the true variables

The shape is the same whether or not the formula was satisfiable — an unsatisfiable result is a data frame with no rows, not a different type — so you can index it without branching first. Every variable the solver knows gets a value, including one no clause constrains; sat_fixed() tells a forced value from a chosen one.

sat_solve(list(1, -1))
#> <zusat_solution> unsat  (1 variable, 0 active clauses, 0.000s)

Enumerating solutions

sat_solutions(list(c(1, 2)))
#> <zusat_solutions> sat  (3 solutions)
#>  solution variable value
#>         1        1  TRUE
#>         1        2  TRUE
#>         2        1 FALSE
#>         2        2  TRUE
#>         3        1  TRUE
#>         3        2 FALSE

Encodings introduce auxiliary variables, and models that differ only in those are usually the same answer repeated. vars projects onto the variables you care about, so each distinct assignment of them is returned once:

sat_n_solutions(sat_solutions(list(c(1, 2)), vars = 1:3))  #> 6
sat_n_solutions(sat_solutions(list(c(1, 2)), vars = 1:2))  #> 3

Enumeration stops at limit (1000 by default, because the count is usually exponential). Check whether it finished:

sols <- sat_solutions(cnf, limit = 100)
sat_complete(sols)   #> FALSE means there may be more

Incremental solving

A solver keeps its state, so adding a clause and re-solving reuses everything already learned. This is where CaDiCaL earns its keep over a one-shot call.

s <- sat_solver(list(c(1, 2)))

sat_solve(s)         #> sat
sat_add(s, -1)       # one clause
sat_add(s, -2)       # ...
sat_solve(s)         #> unsat

sat_solve() works on a formula or a solver, so the calling code reads the same either way.

Assumptions

Assumptions hold for a single call. When the result is unsatisfiable, sat_failed() reports which of them the solver actually used — an unsatisfiable core over the assumptions:

s <- sat_solver(list(c(1, 2)))

sat_solve(s, assumptions = c(-1, -2))   #> unsat
sat_failed(s, c(-1, -2))                #> TRUE TRUE

sat_solve(s)                            #> sat — assumptions did not persist

CaDiCaL does not expose cores over the original clauses, only over assumptions. If you need to know which clauses conflict, encode each one with a selector variable and assume the selectors.

Cardinality constraints

"At most three of these", "exactly one of these" — the constraints most real models are built from. CNF cannot express them directly, so they have to be encoded as clauses:

s <- sat_solver()

sat_exactly(s, 1:4, 1)     # exactly one of x1..x4
sat_at_most(s, 5:12, 2)    # at most two of x5..x12
sat_at_least(s, 13:20, 3)  # at least three of x13..x20

sat_solve(s)

Negative literals work too, so "at most one of these is false" is sat_at_most(s, -(1:4), 1).

The encoding is chosen automatically, and the choice is not marginal — at 40 literals with k = 3, forbidding every 4-subset is 91,390 clauses while a sequential counter is a few hundred. Override it when you are measuring:

sat_at_most(s, 1:40, 3, encoding = "sequential")

These take a solver rather than returning clauses, because every encoding but the pairwise one introduces auxiliary variables that must not collide with the rest of the formula. The solver is the only thing that knows which variables are already in use.

It cannot know which ones you will use later, though. If your model numbers more variables after adding a constraint, reserve the whole range first, so the auxiliaries are allocated above it:

s <- sat_solver()
sat_reserve(s, 24)         # variables 1..24 are ours
sat_exactly(s, 1:12, 1)    # auxiliaries start at 25
sat_exactly(s, 13:24, 1)

Without sat_reserve(), the second constraint would be an error: the solver remembers which variables are auxiliary and refuses them in clauses, assumptions and constraints rather than let the two silently merge.

Bounding a solve

SAT is NP-complete, so an innocuous-looking formula can run far longer than you are willing to wait. A limit makes the solver give up and return "unknown" instead of an answer:

s <- sat_solver(hard_formula)
sat_limit(s, "conflicts", 10000)

sol <- sat_solve(s)
if (sat_status(sol) == "unknown") {
  # gave up within budget -- not the same as unsatisfiable
}

Like assumptions, a limit applies to the next sat_solve() only.

Temporary constraints

Assumptions fix individual literals. A constraint is a whole clause that applies to one solve and is then discarded — useful for asking "what if at least one of these were false?" without permanently changing the formula:

s <- sat_solver(list(c(1, 2)))

sat_constrain(s, c(-1, -2))   # at least one of x1, x2 false
sat_solve(s)
sat_constraint_failed(s)      # did the constraint cause unsat?

sat_solve(s)                  # constraint is gone

A constraint covers one solve, and sat_solutions() solves once per model, so it refuses to start while one is pending. Pass the clause as its constraint argument instead, which applies it to every solve:

sat_solutions(s, constraint = c(-1, -2))

What the solver has already proved

sat_fixed() reports literals true in every model, or false in every model — the formula's backbone as far as the solver has discovered it:

s <- sat_solver(list(1, c(-1, 2)))
sat_solve(s)

sat_fixed(s, c(1, 2, 3))   #> TRUE TRUE NA

sat_simplify() runs CaDiCaL's inprocessing without searching, which occasionally settles a formula outright and otherwise leaves it smaller.

Tuning

CaDiCaL has several hundred integer options:

sat_option(s, "elim")        # read
sat_option(s, "elim", 0)     # disable bounded variable elimination

Proofs of unsatisfiability

When a solver says "unsat", you are taking its word for it. A proof makes the claim checkable by an independent tool — nothing about zusat, CaDiCaL or this binding has to be trusted for the check to mean something.

path <- tempfile(fileext = ".drat")

s <- sat_solver()            # must be empty: tracing records the whole
sat_trace_proof(s, path)     # derivation, so it starts before the clauses
sat_add(s, clauses)
sat_solve(s)                 #> "unsat"
sat_close_proof(s)           # the proof is incomplete until this returns

Then check it with whatever you like:

drat-trim problem.cnf problem.drat
#> s VERIFIED

What the proof refutes is whatever the checker is given, so give it everything the solver had:

• after an "unsat" under assumptions, the proof refutes the formula plus the failed assumptions: add each one (see sat_failed()) to the CNF as a unit clause;
• in incremental use, every clause added while tracing — including the blocking clauses sat_solutions() adds — belongs in the CNF too, since DRAT records only derived clauses.

A satisfiable formula needs no proof — the model is the evidence, and sat_assignment() hands it to you.

format = "lrat" records the antecedents of every step, so a checker verifies it by lookup instead of re-deriving anything: bigger files, much faster and simpler checking.

Interrupting

Long solves respond to Ctrl-C. The solver stops at its next safe point and raises a catchable error; the handle stays usable afterwards.

Updating the bundled solver

tools/vendor-cadical.sh [git-ref] re-vendors CaDiCaL from upstream, applies the R compatibility rewrites, and records the exact commit, a manifest and per-file checksums. tools/vendor/verify checks the tree against them.

Licence

zusat is MIT licensed. The bundled CaDiCaL is also MIT licensed — see inst/CADICAL_LICENSE and inst/COPYRIGHTS.