Skip to content

dirkschumacher/rpicosat

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
R
 
 
 
 
man
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

R-CMD-check CRAN Status Codecov test coverage

rpicosat

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.

Install

Install development version

devtools::install_github("dirkschumacher/rpicosat")

Install stable version from CRAN

install.packages("rpicosat")

API

  • picosat_sat can solve a SAT problem. The result is a data.frame + meta data, so you can use it with dplyr et al.
  • picosat_solution_status applied to the result of picosat_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 #clauses
  • picosat_decisions #decisions
  • picosat_propagations #propagations
  • picosat_seconds seconds spent in the C function picosat_sat
  • picosat_variables #variables
  • picosat_visits #visits

Example

Suppose we want to test the following formula for satisfiability:

(AB) ∧ (BC) ∧ (CA)

This can be formulated as a CNF (conjunctive normal form):

AB) ∧ (¬BC) ∧ (¬CA)

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

License

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.

Other packages

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.

Tests

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%