| Title: | SAT Solver using 'PicoSAT' |
|---|---|
| Description: | A solver for Boolean satisfiability problems ('SAT') using the 'PicoSAT' library. For this solver, 'SAT' problems can be formulated in two ways; using integer literals, or using logical expressions specified with the 'satire' package. |
| Authors: | Mike Cheng [aut, cre, cph], Dirk Schumacher [aut, cph] (Fixes for original picosat.c in rpicosat package), Armin Biere [aut, cph] (Author and copyright holder of included PicoSAT code) |
| Maintainer: | Mike Cheng <[email protected]> |
| License: | MIT + file LICENSE |
| Version: | 1.0.0.9000 |
| Built: | 2026-05-28 10:01:11 UTC |
| Source: | https://github.com/coolbutuseless/picosatire |
Solve simple using literals
pico_solve_literals(literals, max_solutions = 1)pico_solve_literals(literals, max_solutions = 1)
literals |
integer literals |
max_solutions |
limit number of solutions |
Return NULL is problem is unsatisfiable. Otherwise return a list of integer sequences of literals - each sequence is a solution.
pico_solve_literals(c(1, 2, 0, 2, -3, 0))pico_solve_literals(c(1, 2, 0, 2, -3, 0))
Solve simple using 'satire'
pico_solve_satire(sat, max_solutions = 1, remove = "^dummy")pico_solve_satire(sat, max_solutions = 1, remove = "^dummy")
sat |
SAT problem definition as created by |
max_solutions |
limit number of solutions |
remove |
regular expression for variables to remove when blocking solutions and assembling values to return. Default: "^dummy" will block all variables starting with the word "dummy" (as this is how the 'satire' package automatically creates dummy variables.) If NULL no variables will be removed. |
Return NULL is problem is unsatisfiable. Otherwise return a data.frame of solutions where each column represents a named variable in the problem and each row is a solution.
sat <- satire::sat_new() satire::sat_add_exprs(sat, "a -> (b & c)") pico_solve_satire(sat, max_solutions = 10) satire::sat_solve_naive(sat) satire::sat_solve_dpll(sat, max_solutions = 10)sat <- satire::sat_new() satire::sat_add_exprs(sat, "a -> (b & c)") pico_solve_satire(sat, max_solutions = 10) satire::sat_solve_naive(sat) satire::sat_solve_dpll(sat, max_solutions = 10)
Return a list of version information of the PicoSAT library
pico_version()pico_version()
Named list of version information. PICOSAT_API_VERSION is the
internal C API version, and release is the numbering of the
software release tarball.
pico_version()pico_version()