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.
devtools::install_github("dirkschumacher/rpicosat")
install.packages("rpicosat")
picosat_sat
can solve a SAT problem. The result is adata.frame
+ meta data, so you can use it withdplyr
et al.picosat_solution_status
applied to the result ofpicosat_sat
returns 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
solver:
picosat_added_original_clauses
#clausespicosat_decisions
#decisionspicosat_propagations
#propagationspicosat_seconds
seconds spent in the C functionpicosat_sat
picosat_variables
#variablespicosat_visits
#visits
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)
In 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 dplyr
.
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 TRUE
or FALSE
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.70%
#> src/picosat.c: 38.12%
#> R/rpicosat.R: 80.00%
#> src/init.c: 100.00%
#> src/r_picosat.c: 100.00%