# 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:

(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``````

``````covr::package_coverage()