R Bindings for the 'PicoSAT' SAT Solver

Bindings for the 'PicoSAT' solver to solve Boolean satisfiability problems (SAT). The boolean satisfiability problem asks the question if a given boolean formula can be TRUE; i.e. does there exist an assignment of TRUE/FALSE for each variable such that the whole formula is TRUE? The package bundles 'PicoSAT' solver release 965 < http://www.fmv.jku.at/picosat/>.


AppVeyor Build Status Travis-CI Build Status Coverage Status CRAN Status

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

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:

(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

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.09%
#> src/picosat.c: 37.41%
#> R/rpicosat.R: 80.00%
#> src/init.c: 100.00%
#> src/r_picosat.c: 100.00%

News

rpicosat 1.0.1

Bugfixes

  • Fixed potential problems with garbage collection in the C code

rpicosat 1.0.0

  • Initial CRAN release

Reference manual

It appears you don't have a PDF plugin for this browser. You can click here to download the reference manual.

install.packages("rpicosat")

1.0.1 by Dirk Schumacher, a year ago


https://github.com/dirkschumacher/rpicosat


Report a bug at https://github.com/dirkschumacher/rpicosat/issues


Browse source code at https://github.com/cran/rpicosat


Authors: Dirk Schumacher [aut, cre] , Armin Biere [ctb, cph] (Author and copyright holder of included PicoSAT code)


Documentation:   PDF Manual  


MIT + file LICENSE license


Suggests testthat, covr


See at CRAN