{satire} is a package for defining Boolean satisfiability problems
(i.e. SAT problems) and includes two SAT solvers (written in R).
A key feature of this package is that allows for the definition of the SAT problem by specifying the clauses of the Boolean formula as logical expressions. This can allow for a more natural definition of the problem and for remapping of the solution back to the original variable names.
In addition, even though this style of SAT solver usually requires
Boolean formula to be in Conjunctive Normal
Form(CNF),
{satire} will automatically translate non-CNF expressions to CNF using
substitutions and applying Tesytin
transformation.
sat <- sat_new()create a new problem objectsat_add_literals()add integer literals to a problem.sat_add_exprs()add Boolean expressions to a problem. If expressions are not in CNF (conjunctive normal form), then substitution rules and Tseytin transformation will be applied to convert them to CNF.sat_card_*()add cardinality constraints to a problem.sat_card_exactly_one()sat_card_atleast_one()sat_card_atmost_one()sat_card_exactly_k()sat_card_atleast_k()sat_card_atmost_k()
- Report the current state of the problem
sat$dimacssat$literalssat$namessat$exprs
read_dimacs()read in a problem from a standard DIMACs-formatted file- SAT solvers
sat_solve_naive()is a naive solver suitable for problems with ~20 variablessat_solve_dpll()implements basic DPLL solving techniques.
This solver is suitable for use in larger problems, but is written in base R and is not fast.
The two SAT solvers included in this package (sat_solve_naive() &
sat_solve_dpll()) are written in base R and are really for
demonstration and education purposes. They are only suitable for
smaller/easier problems as they are comparatively quite slow.
For larger problems, either export to DIMACS format and use another solver of your choice, or try the following companion R packages:
- picosatire a wrapper for the C SAT solver library PicoSAT
- kissatire a wrapper for the C SAT solver library Kissat (not compatible with windows)
You can install the latest development version from GitHub with:
# install.package('remotes')
remotes::install_github('coolbutuseless/satire')Pre-built source/binary versions can also be installed from R-universe
install.packages('satire', repos = c('https://coolbutuseless.r-universe.dev', 'https://cloud.r-project.org'))This is a demonstration of how {satire} could be used to formulate and
solve a very simple SAT problem.
A, B, C, D are employed by the same company.
The company needs to find all combinations of these employees who can work any given shift given the following constraints:
- Exactly 2 people need to work a shift
- B and D are not allowed to work together
- C must always work with A or D (in order to be trained)
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Create a SAT problem
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat <- sat_new()
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Add constraints
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_k(sat, c('a', 'b', 'c', 'd'), 2) # Exactly two people working
sat_add_exprs(sat, "!b | !d") # B and D not together
sat_add_exprs(sat, "c -> (a | d)") # C must work with A or D
sat#> <sat> vars = 16 , clauses = 28
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# This is a small problem (only 16 variables) so can use the naive solver
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solns <- sat_solve_naive(sat)
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# The solutions are returned as a data.frame.
# - column names correspond to variable names in the problem.
# - each row is a solution
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
solns#> a b c d
#> 1 FALSE FALSE TRUE TRUE
#> 2 TRUE FALSE FALSE TRUE
#> 3 TRUE FALSE TRUE FALSE
#> 4 TRUE TRUE FALSE FALSE
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Extract the names of each pair that can work together
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
apply(solns, 1, function(x) names(solns)[which(x)], simplify = FALSE)#> [[1]]
#> [1] "c" "d"
#>
#> [[2]]
#> [1] "a" "d"
#>
#> [[3]]
#> [1] "a" "c"
#>
#> [[4]]
#> [1] "a" "b"
Problems can be defined in two general ways:
- constructing the problem as an accumulation of Boolean expressions
- constructing the problem as a sequence of literal integers
All of the following are equivalent definitions of a single problem
# Sequential adding of single expressions
sat <- sat_new()
sat_add_exprs(sat, "!a | b")
sat_add_exprs(sat, "!b | c")
sat_add_exprs(sat, "!c | a")
# Adding a vector of expressions
sat <- sat_new()
sat_add_exprs(sat, c("!a | b", "!b | c", "!c | a"))
# Adding a compound expression
sat <- sat_new()
sat_add_exprs(sat, c("(!a | b) & (!b | c) & (!c | a)"))
# Using integer literals
# 1 = a
# -1 = !a
# 2 = b
# -2 = !b
# 3 = c
# -3 = !c
sat <- sat_new()
sat_add_literals(sat, c(-1, 2, 0))
sat_add_literals(sat, c(-2, 3, 0))
sat_add_literals(sat, c(-3, 1, 0))
# Using integer literals, trailing 0 is optional
sat <- sat_new()
sat_add_literals(sat, c(-1, 2))
sat_add_literals(sat, c(-2, 3))
sat_add_literals(sat, c(-3, 1))
# Using literals all in a single vector. Zeros required to separate clauses
sat <- sat_new()
sat_add_literals(sat, c(-1, 2, 0, -2, 3, 0, -3, 1, 0))A common constraint on SAT problems is cardinality i.e. how many different variables can be simultaneously true.
{satire} includes the following helpers to add cardinality constraints
to a SAT problem:
sat_card_exactly_one()sat_card_atleast_one()sat_card_atmost_one()sat_card_exactly_k()sat_card_atleast_k()sat_card_atmost_k()
The encoding for at most one can be done via pairwise encoding (a.k.a binominal encoding) or using commander variables (after Klieber & Kwon).
Coding for at least k, at most k and exactly k uses Sinz’s formulation of LTSeq (See Slide 8).
As an example, the following SAT problem finds combinations from the first 8 letters of the alphabet where exactly 3 are marked as TRUE.
The solution is a data frame where the columns correspond to the variables in the SAT problem, and each row represents a solution.
sat <- sat_new()
sat_card_exactly_k(sat, letters[1:8], 3)
sat#> <sat> vars = 64 , clauses = 118
sat_solve_dpll(sat, max_solutions = 4)#> a b c d e f g h
#> 1 TRUE FALSE TRUE TRUE FALSE FALSE FALSE FALSE
#> 2 FALSE TRUE TRUE TRUE FALSE FALSE FALSE FALSE
#> 3 FALSE FALSE TRUE TRUE TRUE FALSE FALSE FALSE
#> 4 FALSE FALSE TRUE TRUE FALSE TRUE FALSE FALSE
A problem which is unsatisfiable will generate a NULL with the solvers
included in this package (sat_solve_naive() and sat_solve_dpll()).
Below, this unsatisiable problem wants a to be simultaneously TRUE
and FALSE - an impossibility.
sat <- sat_new()
sat_add_exprs(sat, "a")
sat_add_exprs(sat, "!a")
sat_solve_naive(sat) # Unsatisfiable#> NULL
sat_solve_dpll(sat) # Unsatisfiable#> NULL
sat <- read_dimacs("inst/zebra_v155_c1135.cnf")
sat
sat_solve_dpll(sat)- https://github.com/crillab/gophersat/blob/master/examples/sat-for-noobs.md
- https://en.wikipedia.org/wiki/Conjunctive_normal_form
- https://rbcborealis.com/research-blogs/tutorial-9-sat-solvers-i-introduction-and-applications/
- https://smt.st/
- https://personal.cis.strath.ac.uk/robert.atkey/cs208/converting-to-cnf.html - a good video on transforming formulas and the Tseytin transformation.
- https://www.inf.ed.ac.uk/teaching/courses/inf1/cl/2020/week8/