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

## 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%
```