-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.Rmd
116 lines (79 loc) · 2.96 KB
/
README.Rmd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
---
output:
md_document:
variant: gfm
---
<!-- badges: start -->
[![R-CMD-check](https://github.com/dirkschumacher/rpicosat/workflows/R-CMD-check/badge.svg)](https://github.com/dirkschumacher/rpicosat/actions)
[![CRAN Status](http://www.r-pkg.org/badges/version/rpicosat)](https://CRAN.R-project.org/package=rpicosat)
[![Codecov test coverage](https://codecov.io/gh/dirkschumacher/rpicosat/branch/master/graph/badge.svg)](https://app.codecov.io/gh/dirkschumacher/rpicosat?branch=master)
<!-- badges: end -->
```{r, echo = FALSE}
knitr::opts_chunk$set(
collapse = TRUE,
comment = "#>",
fig.path = "README-"
)
```
# rpicosat
R bindings to the [PicoSAT solver release 965](http://fmv.jku.at/picosat/) by Armin Biere. The PicoSAT C code is distributed under a MIT style license and is bundled with this package.
## Install
### Install development version
```{r, eval=FALSE}
devtools::install_github("dirkschumacher/rpicosat")
```
### Install stable version from CRAN
```{r, eval = FALSE}
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 \Rightarrow B) \wedge (B \Rightarrow C) \wedge (C \Rightarrow A)
$$
This can be formulated as a CNF (conjunctive normal form):
$$
(\neg A \vee B) \wedge (\neg B \vee C) \wedge (\neg C \vee A)
$$
In `rpicosat` the problem is encoded as a list of integer vectors.
```{r}
formula <- list(
c(-1, 2),
c(-2, 3),
c(-3, 1)
)
```
```{r example}
library(rpicosat)
res <- picosat_sat(formula)
res
```
Every result is also a `data.frame` so you can process the results with packages like `dplyr`.
```{r}
as.data.frame(res)
```
We can also test for satisfiability if we assume that a certain literal is `TRUE` or `FALSE`
```{r}
picosat_sat(formula, c(1)) # assume A is TRUE
```
```{r}
picosat_sat(formula, c(1, -3)) # assume A is TRUE, but C is FALSE
```
## 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](https://github.com/search?utf8=✓&q=picosat) providing bindings to PicoSAT. After writing this package I discovered [another package](https://github.com/dtimes6/Rpicosat) on github providing bindings to PicoSAT in R.
## Tests
```{r}
covr::package_coverage()
```