| Title: | SAT Solver using 'Kissat' |
|---|---|
| Description: | A solver for Boolean satisfiability problems ('SAT') using the 'Kissat' 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] |
| Maintainer: | Mike Cheng <[email protected]> |
| License: | MIT + file LICENSE |
| Version: | 1.0.0.9000 |
| Built: | 2026-05-27 10:06:30 UTC |
| Source: | https://github.com/coolbutuseless/kissatire |
Solve using literals
kis_solve_literals(literals, max_solutions = 1)kis_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.
kis_solve_literals(c(1, 2, 0, 2, -3, 0))kis_solve_literals(c(1, 2, 0, 2, -3, 0))
Solve using 'satire'
kis_solve_satire(sat, max_solutions = 1, remove = "^dummy")kis_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)") kis_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)") kis_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 kisSAT library
kis_version()kis_version()
Named list of version information. kisSAT_API_VERSION is the
internal C API version, and release is the numbering of the
software release tarball.
kis_version()kis_version()