---
title: "introduction"
output: rmarkdown::html_vignette
vignette: >
  %\VignetteIndexEntry{introduction}
  %\VignetteEngine{knitr::rmarkdown}
  %\VignetteEncoding{UTF-8}
---

```{r, include = FALSE}
knitr::opts_chunk$set(
  collapse = FALSE,
  comment = "#>"
)
```

```{r setup}
library(satire)
```


# satire

`{satire}` is a package for defining Boolean satisfiability problems (i.e. SAT problems)
and includes two pure R SAT solvers.

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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form), 
`{satire}` will automatically translate non-CNF expressions to CNF using
substitutions and applying [Tesytin transformation](https://en.wikipedia.org/wiki/Tseytin_transformation).


### What's in the box

* `sat <- sat_new()` create a new problem object
* `sat_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$dimacs`
    * `sat$literals`
    * `sat$names`
    * `sat$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 variables
    * `sat_solve_dpll()` implements basic [DPLL](https://en.wikipedia.org/wiki/DPLL_algorithm) solving techniques.  
      This solver is suitable
      for use in larger problems, but is written in base R and is not fast.


## SAT Solvers

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](https://github.com/coolbutuseless/picosatire) a wrapper for the C
  SAT solver library PicoSAT
* [kissatire](https://github.com/coolbutuseless/kissatire) a wrapper for the C
  SAT solver library Kissat  (not compatible with windows)
  


### SAT Example: Finding all possible work teams

This is a demonstration of how `{satire}` could be used to formulate and 
solve a very simple SAT problem.

#### Problem statement

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)

```{r}
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 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 B or D
sat

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 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

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Extract the names of each pair that can work together
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
apply(solns, 1, function(x) names(solns)[which(x)], simplify = FALSE)
```



### Tools for defining a problem

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

```{r eval = TRUE}
# 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))
```



### Cardinality helpers

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.


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.

```{r eval=TRUE}
sat <- sat_new()
sat_card_exactly_k(sat, letters[1:8], 3)
sat
sat_solve_dpll(sat, max_solutions = 4)
```


## Unsatisfiable problem example

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.

```{r}
sat <- sat_new()
sat_add_exprs(sat, "a")
sat_add_exprs(sat, "!a")
sat_solve_naive(sat) # Unsatisfiable
sat_solve_dpll(sat)  # Unsatisfiable
```



## Solving a problem from a DIMACs file

```{r eval = FALSE}
sat <- read_dimacs("inst/zebra_v155_c1135.cnf")
sat

sat_solve_dpll(sat)
```