picosat_sat: Solve SAT problems with the 'PicoSAT' solver

Description Usage Arguments Value References Examples

View source: R/rpicosat.R

Description

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.

Usage

1
picosat_sat(formula, assumptions = integer(0L))

Arguments

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.

Value

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.

References

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.

Examples

 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)

rpicosat documentation built on May 1, 2019, 8:41 p.m.