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

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

**Any scripts or data that you put into this service are public.**

Embedding an R snippet on your website

Add the following code to your website.

For more information on customizing the embed code, read Embedding Snippets.