R bindings to the PicoSAT solver release 965 by Armin Biere. The PicoSAT C code is distributed under a MIT style license and is bundled with this package.
picosat_satcan solve a SAT problem. The result is a
data.frame+ meta data, so you can use it with
picosat_solution_statusapplied to the result of
picosat_satreturns either PICOSAT_SATISFIABLE, PICOSAT_UNSATISFIABLE or PICOSAT_UNKNOWN
The following functions can be applied to solutions and make available some statistics generated by the
picosat_secondsseconds spent in the C function
Suppose we want to test the following formula for satisfiability:
(A ⇒ B)∧(B ⇒ C)∧(C ⇒ A)
This can be formulated as a CNF (conjunctive normal form):
(¬A ∨ B)∧(¬B ∨ C)∧(¬C ∨ A)
rpicosat the problem is encoded as a list of integer vectors.
formula <- list( c(-1, 2), c(-2, 3), c(-3, 1) )
library(rpicosat) res <- picosat_sat(formula) res #> Variables: 3 #> Clauses: 3 #> Solver status: PICOSAT_SATISFIABLE
Every result is also a
data.frame so you can process the results with packages like
as.data.frame(res) #> variable value #> 1 1 FALSE #> 2 2 FALSE #> 3 3 FALSE
We can also test for satisfiability if we assume that a certain literal is
picosat_sat(formula, c(1)) # assume A is TRUE #> Variables: 3 #> Clauses: 3 #> Solver status: PICOSAT_SATISFIABLE
picosat_sat(formula, c(1, -3)) # assume A is TRUE, but C is FALSE #> Solver status: PICOSAT_UNSATISFIABLE
This R package is licensed under MIT. The PicoSAT solver bundled in this package is licensed MIT as well: Copyright (c) Armin Biere, Johannes Kepler University.
There are numerous other packages providing bindings to PicoSAT. After writing this package I discovered another package on github providing bindings to PicoSAT in R.
covr::package_coverage() #> rpicosat Coverage: 39.09% #> src/picosat.c: 37.41% #> R/rpicosat.R: 80.00% #> src/init.c: 100.00% #> src/r_picosat.c: 100.00%