| Title: | Define and Solve Boolean Satisfiability ('SAT') Problems |
|---|---|
| Description: | Boolean satisifiability ('SAT') tests whether there are sets of variables which satisfy a Boolean formula. This package provides tools for defining 'SAT' problems and includes a 'DPLL'-based 'SAT' solver based upon Davis & Putnam (1960) <doi:10.1145/321033.321034>. Built-in capabilities for Tseytin transformation (Tseytin (1968) <doi:10.1007/978-3-642-81955-1_28>) allows for the input of complex Boolean formula. Cardinalility constraints are implemented using commander variables (Klieber & Kwon (2007) <https://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf>) and sequential counters (Sinz (2005) <doi:10.1007/11564751_73>). Tools for reading and writing 'DIMACS' files are also included. |
| Authors: | Mike Cheng [aut, cre, cph] |
| Maintainer: | Mike Cheng <[email protected]> |
| License: | MIT + file LICENSE |
| Version: | 1.0.0.9000 |
| Built: | 2026-06-03 10:50:06 UTC |
| Source: | https://github.com/coolbutuseless/satire |
Expression may include nesting with brackets, &, |, !,
-> (implication) and == (equivalence). All other elements in
the expression must be names. Names must only contain a-z, A-Z, 0-9 and underscore.
as_cnf(expr, dummy_idx = 1L)as_cnf(expr, dummy_idx = 1L)
expr |
Boolean expression |
dummy_idx |
starting index for dummy numbering. If the supplied expression
is not in CNF, then Tseytin transform may be applied, and this often
generates extra dummy variables. In order to avoid variable name
clashes it is necessary for the caller to provide a |
string containing an expression in CNF
as_cnf("a | b") # Already CNF. returns the argument unchanged as_cnf("a -> b") # Rewrite via substitution as_cnf("!!a & b") # Rewrite via substitution as_cnf("!(a | b)") # Uses Tseytin transformas_cnf("a | b") # Already CNF. returns the argument unchanged as_cnf("a -> b") # Rewrite via substitution as_cnf("!!a & b") # Rewrite via substitution as_cnf("!(a | b)") # Uses Tseytin transform
Determine if the expression (in a string) is in conjunctive normal form
is_cnf(s)is_cnf(s)
s |
single string containing an expression |
Logical value. TRUE if expression is a CNF. Return FALSE if expression is a valid boolean formula but is not in CNF. Otherwise an error is raised.
# Expect TRUE for these CNF expressions is_cnf("a | !b") is_cnf("(a | !b) & (c | d | e)") # Expect FALSE for these expressions is_cnf("!!a") is_cnf("!(a & b)") is_cnf("!(a | b)") is_cnf("a & (b | (d & e))")# Expect TRUE for these CNF expressions is_cnf("a | !b") is_cnf("(a | !b) & (c | d | e)") # Expect FALSE for these expressions is_cnf("!!a") is_cnf("!(a & b)") is_cnf("!(a | b)") is_cnf("a & (b | (d & e))")
Convert literals to a DIMACS-formatted string
literals_to_dimacs(literals)literals_to_dimacs(literals)
literals |
integer vector of positive and negative literal values. Clauses should be separated using zero (0). If the vector is not terminated by a zero (0), then a zero will be added. |
Character string holding the DIMACS representation
sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") literals_to_dimacs(sat$literals)sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") literals_to_dimacs(sat$literals)
literals_to_dimacs()
Print a DIMACs representation returned from literals_to_dimacs()
## S3 method for class 'sat_dimacs' print(x, ...)## S3 method for class 'sat_dimacs' print(x, ...)
x |
|
... |
ignored |
None
literals <- c(1, 2, 3, 0, -2, 4, 0, 5, 6, 7, 0) dimacs <- literals_to_dimacs(literals) dimacsliterals <- c(1, 2, 3, 0, -2, 4, 0, 5, 6, 7, 0) dimacs <- literals_to_dimacs(literals) dimacs
Print 'sat' object
## S3 method for class 'sat_prob' print(x, ...)## S3 method for class 'sat_prob' print(x, ...)
x |
'sat' object created by |
... |
ignored |
Invisible copy of original x
sat <- sat_new() print(sat)sat <- sat_new() print(sat)
sat object.This function reads SAT data from standard DIMACS files. Any comment lines (lines starting with 'c') are ignored.
read_dimacs(filename)read_dimacs(filename)
filename |
filename with CNF in DIMACS format |
sat object
filename <- system.file("sudoku.cnf", package = 'satire', mustWork = TRUE) sat <- read_dimacs(filename = filename) sat sat$literals[1:100]filename <- system.file("sudoku.cnf", package = 'satire', mustWork = TRUE) sat <- read_dimacs(filename = filename) sat sat$literals[1:100]
Note: Adding clauses to a SAT problem can only be via adding integer literals
(via sat_add_literals()) or adding named expressions (via
sat_add_exprs()) . The two
methods cannot be mixed within a single SAT problem.
sat_add_exprs(sat, exprs, verbosity = 0L)sat_add_exprs(sat, exprs, verbosity = 0L)
sat |
|
exprs |
a character vector of Boolean expressions - liberal use brackets is encouraged to signify intent. If any expression is not in CNF, an attempt will be made to convert it to CNF using Tseytin transformation. Allowed syntax:
|
verbosity |
Verbosity level. Default: 0 |
None
Other ways of adding clauses:
sat_add_literals()
# Solve a small SAT problem using strings sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") sat_solve_naive(sat) # Multiple string clauses may be added a single call. sat <- sat_new() sat_add_exprs(sat, c("!a | b", "!b | c", "!c | a")) sat_solve_naive(sat)# Solve a small SAT problem using strings sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") sat_solve_naive(sat) # Multiple string clauses may be added a single call. sat <- sat_new() sat_add_exprs(sat, c("!a | b", "!b | c", "!c | a")) sat_solve_naive(sat)
Note: Adding clauses to a SAT problem can only be via adding integer literals
(via sat_add_literals()) or adding named expressions (via
sat_add_exprs()) . The two
methods cannot be mixed within a single SAT problem.
sat_add_literals(sat, literals)sat_add_literals(sat, literals)
sat |
|
literals |
integer vector of positive and negative literal values. Clauses should be separated using zero (0). If the vector is not terminated by a zero (0), then a zero will be added. |
None
Other ways of adding clauses:
sat_add_exprs()
# Define a small SAT problem sat <- sat_new() sat_add_literals(sat, c(-1, 2)) sat_add_literals(sat, c(-2, 3)) sat_add_literals(sat, c(-3, 1)) sat_solve_naive(sat) # Equivalent problem sat <- sat_new() sat_add_literals(sat, c(-1, 2, 0, -2, 3, 0, -3, 1, 0)) sat_solve_naive(sat)# Define a small SAT problem sat <- sat_new() sat_add_literals(sat, c(-1, 2)) sat_add_literals(sat, c(-2, 3)) sat_add_literals(sat, c(-3, 1)) sat_solve_naive(sat) # Equivalent problem sat <- sat_new() sat_add_literals(sat, c(-1, 2, 0, -2, 3, 0, -3, 1, 0)) sat_solve_naive(sat)
Block a given result - use this for manually finding multiple solutions to a given problem.
sat_block_solution(sat, literals, verbosity = 0L)sat_block_solution(sat, literals, verbosity = 0L)
sat |
|
literals |
A solution. Vector of integer literals. |
verbosity |
verbosity |
None
# Setup a problem and solve sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") sat_solve_naive(sat) # Block the solution where all values are TRUE soln1 <- "a & b & c" # Block this solution from occurring sat_block_solution(sat, soln1) # Now only a single solution returned sat_solve_naive(sat)# Setup a problem and solve sat <- sat_new() sat_add_exprs(sat, "!a | b") sat_add_exprs(sat, "!b | c") sat_add_exprs(sat, "!c | a") sat_solve_naive(sat) # Block the solution where all values are TRUE soln1 <- "a & b & c" # Block this solution from occurring sat_block_solution(sat, soln1) # Now only a single solution returned sat_solve_naive(sat)
This constraint is an implementation of Sinz's LTseq formulation.
sat_card_exactly_k(sat, nms, k) sat_card_atleast_k(sat, nms, k) sat_card_atmost_k(sat, nms, k)sat_card_exactly_k(sat, nms, k) sat_card_atleast_k(sat, nms, k) sat_card_atmost_k(sat, nms, k)
sat |
|
nms |
character vector of variable names |
k |
k limit |
a character vector of expression strings representing the cardinality constraint in conjunctive normal form
Other SAT cardinality constraints:
sat_card_exactly_one()
sat <- sat_new() sat_card_exactly_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprs sat <- sat_new() sat_card_atleast_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprs sat <- sat_new() sat_card_atmost_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprssat <- sat_new() sat_card_exactly_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprs sat <- sat_new() sat_card_atleast_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprs sat <- sat_new() sat_card_atmost_k(sat, c('a', 'b', 'c', 'd'), k = 2) sat$exprs
Add to SAT problem the cardinality constraint for "exactly one", "at most one" or "at least one" of the given variables is true
sat_card_exactly_one(sat, nms, method = "pairwise") sat_card_atleast_one(sat, nms) sat_card_atmost_one(sat, nms, method = "pairwise")sat_card_exactly_one(sat, nms, method = "pairwise") sat_card_atleast_one(sat, nms) sat_card_atmost_one(sat, nms, method = "pairwise")
sat |
|
nms |
character vector of variable names |
method |
nethod to use to encode this constraint. Default: 'pairwise'
|
a character vector of expression strings representing the cardinality constraint in conjunctive normal form
Other SAT cardinality constraints:
sat_card_exactly_k()
sat <- sat_new() sat_card_exactly_one(sat, c('a', 'b', 'c', 'd')) sat$exprs sat <- sat_new() sat_card_atleast_one(sat, c('a', 'b', 'c', 'd')) sat$exprs sat <- sat_new() sat_card_atmost_one(sat, c('a', 'b', 'c', 'd')) sat$exprssat <- sat_new() sat_card_exactly_one(sat, c('a', 'b', 'c', 'd')) sat$exprs sat <- sat_new() sat_card_atleast_one(sat, c('a', 'b', 'c', 'd')) sat$exprs sat <- sat_new() sat_card_atmost_one(sat, c('a', 'b', 'c', 'd')) sat$exprs
Copy a SAT problem
sat_copy(sat)sat_copy(sat)
sat |
Original SAT problem |
Copy of SAT problem
sat <- sat_new() sat_add_literals(sat, c(1, 2)) sat2 <- sat_copy(sat) sat_add_literals(sat, c(3, 4)) sat sat2sat <- sat_new() sat_add_literals(sat, c(1, 2)) sat2 <- sat_copy(sat) sat_add_literals(sat, c(3, 4)) sat sat2
This function is used when a set of literals (Usually corresponding to a solution) needs to be turned into a logical statement with named variables.
sat_literals_to_lgl(sat, literals, remove = "^dummy")sat_literals_to_lgl(sat, literals, remove = "^dummy")
sat |
|
literals |
literals |
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. |
Named logical vector indicating the names and boolean values of the given literals
sat <- sat_new() sat_add_exprs(sat, c("(a | !b) & (!c | !d)")) sat$names sat$named_literals sat_literals_to_lgl(sat, c(1, 3, -4))sat <- sat_new() sat_add_exprs(sat, c("(a | !b) & (!c | !d)")) sat$names sat$named_literals sat_literals_to_lgl(sat, c(1, 3, -4))
Initialise a new SAT problem
sat_new()sat_new()
sat object
sat <- sat_new() sat sat_add_literals(sat, c(1, 2)) sat_add_literals(sat, c(2, -3)) sat sat$names sat$named_literals sat$exprs sat$dimacs sat_solve_naive(sat)sat <- sat_new() sat sat_add_literals(sat, c(1, 2)) sat_add_literals(sat, c(2, -3)) sat sat$names sat$named_literals sat$exprs sat$dimacs sat_solve_naive(sat)
This pure R recursive solver uses DPLL methods (unit propagation and pure literal elimination). This solver works recursively and can be used to solve problems with 10s to 100s of variables. However, as all the code is in R, this is not as fast as using a compiled solver.
sat_solve_dpll(sat, max_solutions = 1, remove = "^dummy", verbosity = 0L)sat_solve_dpll(sat, max_solutions = 1, remove = "^dummy", verbosity = 0L)
sat |
SAT problem as created by |
max_solutions |
maximum number of solutions to return. Default: 1 |
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. |
verbosity |
verbosity level. Default: 0 |
For larger problems >100 variables, it may better to export the problem as a DIMACS file and solve externally.
data.frame of logical values. Columns correspond to the variable names within the problem. Each row defines a solution.
Other SAT solvers:
sat_solve_naive()
sat <- sat_new() sat_card_atmost_k(sat, letters[1:4], 3) sat$exprs sat$names sat_solve_naive(sat) sat_solve_dpll(sat, max_solutions = 20)sat <- sat_new() sat_card_atmost_k(sat, letters[1:4], 3) sat$exprs sat$names sat_solve_naive(sat) sat_solve_dpll(sat, max_solutions = 20)
This solver is only suitable for small problems as memory use is exponential in the number of variables and all memory is pre-allocated. E.g. a problem with 21 variables will pre-allocate about a gigabyte of memory. Each extra variable doubles the memory required - e.g. a problem with 32 variables would require allocation of 520 GB of memory.
sat_solve_naive(sat, remove = "^dummy", mem_limit = 1024, verbosity = 0L)sat_solve_naive(sat, remove = "^dummy", mem_limit = 1024, verbosity = 0L)
sat |
SAT problem as created by |
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. |
mem_limit |
only run problems if the estimated memory allocation is less than this number of MB. Default: 1024. This is a guard to prevent catastrophic consequences of trying to allocate too much memory if given a large problem. |
verbosity |
verbosity level. Default: 0 |
data.frame of logical values. Columns correspond to the variable names within the problem. Each row defines a solution. If problem is unsatisfiable, return NULL.
Other SAT solvers:
sat_solve_dpll()
sat <- sat_new() sat_card_atmost_k(sat, letters[1:4], 3) sat$exprs sat$names sat_solve_naive(sat)sat <- sat_new() sat_card_atmost_k(sat, letters[1:4], 3) sat$exprs sat$names sat_solve_naive(sat)
Convert a boolean formula to CNF using Tseytin's transformation
tseytin_transform(expr, dummy_idx = 1L)tseytin_transform(expr, dummy_idx = 1L)
expr |
expression (as string or language object) |
dummy_idx |
value to use for numbering the dummy variables. |
character vector of expressions in conjunctive normal form
tseytin_transform("a | (b & c)") tseytin_transform("!(a | b)")tseytin_transform("a | (b & c)") tseytin_transform("!(a | b)")