# 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/>.

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.

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

Every result is also a `data.frame` so you can process the results with packages like `dplyr`.

We can also test for satisfiability if we assume that a certain literal is `TRUE` or `FALSE`

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

# rpicosat 1.0.1

## Bugfixes

• Fixed potential problems with garbage collection in the C code

# rpicosat 1.0.0

• Initial CRAN release

# Reference manual

install.packages("rpicosat")

1.0.1 by Dirk Schumacher, 3 years 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