Description Usage Arguments Value References Examples
The solver takes a formula in conjunctive normal form and finds a satisfiable assignment of the literals or returns that the formula is not satisfiable.
1 | picosat_sat(formula, assumptions = integer(0L))
|
formula |
a list of integer vectors. Each vector is a clause. Each integer identifies a literal. No element must be 0. Negative integers are negated literals. |
assumptions |
an optional integer vector. Assumptions are fixed values for literals in your formula. Each element corresponds to a literal. Negative literals are FALSE, positive TRUE. |
a data.frame with two columns, variable and value. In case the solution status is not PICOSAT_SATISFIABLE the resulting data.frame has 0 rows. You can use 'picosat_solution_status' to decide if the problem is satisfiable.
PicoSAT version 965 by Armin Biere: http://fmv.jku.at/picosat/
A. Biere. PicoSAT Essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4:75<e2><80><93>97, 2008.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 | # solve a boolean formula
# (not a or b) and (not b or c)
# each variable is an integer
# negations are negative integers
formula <- list(
c(-1L, 2L),
c(-2L, 3L)
)
res <- picosat_sat(formula)
picosat_solution_status(res)
# set a variable to a fixed value
# e.g. a = TRUE and b = TRUE
res <- picosat_sat(formula, assumptions = c(1L, 2L))
picosat_solution_status(res)
# get further information about the solution process
picosat_variables(res)
picosat_added_original_clauses(res)
picosat_decisions(res)
picosat_propagations(res)
picosat_visits (res)
picosat_seconds(res)
|
Add the following code to your website.
For more information on customizing the embed code, read Embedding Snippets.