# SAT

Semantic classification of formulas
---
- valid $\leftrightarrow$ tautology
- satisfiable
- unsatisfiable (contradiction)

Tseitin's encoding
---
- Encoding that can be easily converted into CNF (propositional)
- equi-satisfiable not equivalent
- linear time and space
- new variables are added

Next: Algorithm
---

- build tree out of formula
- give every non leaf node a new variable $h_i$
- add constraints to define these new variables $(h_i \leftrightarrow (a \text{ operator } h_{i+1}))$
- enforce truth of root node $h_1$

Resolution
---
Algorithm for solving Propositional CNF

Next Algorithm:
---

- In predefined order emilinate each variable after each other
- Iff only occuring either positive or negative remove all clauses with that variable
- Else use every pair of positive with negative: Add every variable of both clauses without the one to remove into a new one

SAT Algorithms
---
- Enumeration Algorithm
- DPLL Algorithm
- DPLL + CDCL

Next: Enumeration Algorithm
---
- Bruteforce
- Asign each variable a value
- Use a stack to determine the next variable to change

Next: The DPLL Algorithm
---
Normal Enumeration Alogorithm, but after each decision (and once at the start) use BCP (Boolean constraint propagation)

Next: DPLL + CDCL
---
DPLL Alglrithm, but with conflict resolution and clause learning. Replace backtrack with resolve_conflict

Decison heuristics
---
- Dynamic Largest Individual Sum (DLIS)
- Jeroslow-Wang method
- Variable state independent decaying sum (VSIDS)

Next: Dynamic Largest Individual Sum (DLIS)
---
- Dynamic decision heuristic

For each literal (both positive or negative) check how many clauses with that literal in it are unresolved (i.e. will become positive if used). Then use the variable with the maximum and asign based on the coosen literal.

Next: Jeroslow-Wang method
---
- Static decision heuristic
- Compute: $\sum_{\text{clause }c | l \in c} 2^{-|c|}$ for every literal
- Gives higher weight to literals in shorter clauses.
- Order in max to min

Next: VSIDS
---
- quasi-static decision heuristic (because it changes, but not dependend on the current assignment)

Have counters for each variable. Define increment value (e.g. to 1).
If a variable occurs in a conflict increment it's counter by the increment value. Increment the increment value. For a decision take the variable with the highest value.

Boolean Constraint Propagation
---
A partial assignment to a clause can be:
- unit (all but one literal asigned, but not satisfied)
- satisfied
- unsatisfied
- unresolved (if not anything else)

Antecedent(l) = unit clause implying the value of l

Next: BCP with watched literals
---
Instead of watching every literal in every clause choose two literals out of very clause to watch.
They have to be either both unassigned or one of them true
That way the corresponding clause is neither unit nor unsatisfied
If one of them changes look at the clause.

Implication graph
---
- Graph with decisions as nodes
- Nodes are named "x = v@d" with v = value and d = decision level
- edges are named after clauses, that lead to the decision (by implying)
- Extra node $\kappa$ as a conflict

Conflict resolution (with the implication graph)
---
- Conflict clause: Unstaisfied clause, that is necessary for the satisfaction of the formula; a good one should include the UIP
- Asserting clause: conflict clause with a single literal form the current decision level (becomes unit after one backtrack)
- Unique implication point (UIP) all paths from last decision to $\kappa$ go through that point
- First UIP is the one closest to $\kappa$

Next: Asserting clause finding with resolution
---
To get an asserting conflict clause do the following:

While Clause not yet asserting
    Apply resolution with the antecedent of the last assigned literal

**Example:**
Assignment order: $x_4, x_5, x_6, x_7$
T1 = Res(conflict clause, antecedent of $x_7$, $x_7$)
T2 = Res(T1, antecedent of $x_6$, $x_6$)
...

Unsatisfiable core
---
An *unsatisfiable core* of an unsatisfiable CNF formula is an unsatisfiable subset of the original set of clauses.

Eager vs Lazy SMT solving
---
**Eager:**
transform logical formulas to satisfiable equivalent propositional logic formulas and apply SAT (theory first )

**Lazy:**
use a SAT solver to find solutions for the Boolean skeleton of the formula and a theory solver to check satisfiablility in the underlying theory (theory later)

Full Lazy:
SAT solver for boolean skeleton, Theory solver for constraints solving. If the theory solver fails add boolean constraint on why it failed. After both satisfy return *satisfiable*, if the SAT solver fails return *unsatisfiable*.

Less lazy:
SAT solver gives partial solution. Theory solver checks that. If full solution is reached it's SAT else UNSAT.

Equality logic *without* uninterpreted functions
---
Idea is to check the transitive closure

Next: Algorithm
---
Every variable has an own equivalence class

For every equality:
- Merge the two equivalence classes of the variables used

For every inequality:
- Check whether the two variables are in separate equivalence classes

Equality logic with uninterpreted functions (EQ + UF)
---
We can reduce equility logic with uninterpreted functions to equality logic without uninterpreted functions. This can be done using the Ackerman reduction

We can also do the transitive closure idea, but if we merge $x$ and $y$ also merge $F(x)$ and $F(y)$ for every occuring function $F$ iff existing.

Next: Ackerman reduction
---
$\varphi_{flat}$ is the flattening, where each function application is replaces by a new variable.

$\varphi_{cong}$ is a conjunction of constraints over those new variables that assures functional congruence.

$\varphi^{UF} \equiv \varphi^{EQ} := \varphi_{flat} \land \varphi_{cong}$

To check validity we test for the satisfiablility of
$\varphi^{EQ} := \varphi_{cong} \land \lnot \varphi_{flat}$

Next: Ackerman reduction algorithm
---
For each $F(x_1, ..., x_n)$ in $\varphi$ replace with $F_i$ to get $\varphi_{flat}$ and remember $F(x_1, ..., x_n) \leftrightarrow F_i$.

For each $F(x_1, ..., x_n) \leftrightarrow F_i, F(x'_1, ..., x'_n) \leftrightarrow F_j$ pair:
let $\varphi_{cong} = \varphi_{cong} \land \bigwedge((\bigwedge_{k} x_k = x'_k) \rightarrow F_i = F_j)$

Equality graphs
---
Every variable is a node. They are connected either in a positive way (equality) or negative (disequality).

Equality path: A path that uses no disequality edges is an equality path: $x=^* z$

Disequaltiy path: A path that uses exactly one disequality edge is a disequality path: $x \not=^* z$

Contradictory cycle: A cycle with exactly one disequality edge

Simple cycle: Cycle with pairwise disjunct nodes

Next: The sparse method on polar E-Graphs
---
- Replace all equalities with a boolean variable (negated one for disequalities)
- For each simple contradictory cycle in the equality graph add a transitivity constraint (One of the edges in the cycles must be false)

$\Rightarrow$ exponential number of simple contradictory cycles possible

Next: Non polar E-graphs
---
Non-polar: no positive or negative edges (just edges)

Chordal: Every cycle is either a triangle or has a chord
- Construct boolean skeleton
- Make a non-polar graph and make it chordal
- For each triangle add transitivity constraints ($e_{i,j} \land e_{j,k} \rightarrow e_{i,k}$)

Bitvector Arithmetic
---

- Formulas with bitvectors and arithmatic operations
- Solving via bit-blasting (transform for SAT) (eager)

Next: Operations
---

With bitvector $x$:
- $x_{[l]U}$: unsigned encoding
- $x_{[l]S}$: signed encoding in two complement (highest bit is negative)

Example:
$1001_U = 8 + 0 + 0 + 1$
$1001_S = -8 + 0 + 0 + 1$

> Bit vector arithmetic uses modulo operations

Next: Decidability
---
With unbounded width: undecidable
With bounded width: NP-complete

Next: Bit-Blasting
---
We encode each operation bit-wise with a constraint. For that we might introduce new variables

Easiy for bit-wise or, hard for addition, very hard (near unsolvable) for multiplication

Quantifier-free linear real arithmatic
---
- Input in CNF
- Change all negated constraints to non negated ones ($\lnot (x > y) = (x \leq y)$)
- Solve the boolean skeleton and then theory solve the true constraints

All constraints are of the form $b \sim \sum_k a_k \cdot x_k$, with $a_k$ constant and $x_l$ variable

Next: Gauß variable elimination
---
Used to remove variables or constraints for each equasion constraint.

$\sum a_k \cdot x_k = b$
$\Rightarrow a_j \cdot x_j = b_i - \sum_{\text{without }j} a_k \cdot x_k$
$\Rightarrow x_j = \frac{b_i}{a_j} -\sum_{\text{without }j} \frac{a_k}{a_j} \cdot x_k =: \beta_j$
Now replace all occurences of $x_j$ with $\beta_j$ in all constraints

Next: Fourier-Motzkin
---
Based on variabel elimination

If any of the bounds is strict we add a strict vound

- Choose variable $x_i$
- For each inequality collect lower and upper bounds from the inequalities (lower $\rightarrow \beta \leq x$)
- Require each lower bound to be less that or equal to each upper bound

Next: Algorithm
---
- Remove variables that are not bounded both ways

For each variable x
    For each pair of lower bound l and upper bound u for x
        Add l <= u as constraint
    remove all original constraints containing x

Simplex Method
---
Input: linear real-arithmatic constraints
Problem: SAT or UNSAT

- no strict inequalities
- equalities are transformed into inequalities

Next: Algorithm
---
- Transform into general form
$\sum a x \sim b$ to $\sum ax - s = b$ and $s \sim b$

Basic and non-basic variables
- Basic are dependent (on the left side)

At the start slack variables are basic and variables are non-basic

During the Algorithm we maintain:
- The tableaut
- asn assignment of all variables (including slack variables)

And the invariants are maintaints:
- $A \cdot x = 0 \rightarrow$ all constraints are satisfied
- All non-basic variables satisfy their bounds

Set all assignments to $0$
If a basic variable violates a bound $\rightarrow$ pivot

Bland's rule assures termination (order of variables)

Next: Pivoting
---

- Find a basic variables $x_i$ that violates its bound
- Find a non-basic variables $x_j$ such that (not yet on either bound):
- $a_{ij} > 0$ and $x_j <$ upper bound
- $a_{ij} < 0$ and $x_j >$ lower bound

To pivot x and y transform each equasion correspondingly

**Example:** How to pivot $s_1$ and $x$:
1. solve the $s_1$ row for $x$
2. for every other row replace x with the solved formula
3. set $s_1$ to its lower bound
4. update all basic variables value

Next: Geographic interpretation
---
A solution is equvalent to a convex polyhidra in a k-dimensional space.
Easier in two dimensions. Into a coordinate-system draw constraints as lines with arrows. The arrows point towards the *unsatisfiable* side.

Integer linear systems
---

General form constraint with integer as variables.

Next: Algorithm
---
- Solve without the integer requirement
- for each non integer variable x with value r:
- recursive call with additional constraint $x \leq floor(r)$
- recursive call with additional constraint $x \geq ceil(r)$

This algorithm is incomplete (does not halt on every input), can be adjusted to be complete

Requirements on the theory solver
---
- Incrementality: we increase a set of constraints, so the solver should make use of the previous SAT-check for the analysis
- (Preferably minimal) infeasible subsets: if the set is infeasible compute a reason for unsatisfaction
- backtracking: the theory solver should be able to remove constraints (in inverse chronological order)

Interval constraint propagation
---

- incomplete

Next: Interval operations
---
**Addition:**
- Add each bound separately

**Subtraction:**
- \[lower - upper; upper - lower\]

**Multiplication:**
- \[min(all multiplications); max(all multiplications)\]
- Squaring can only result in positive values

**Square root:**
- [-$\sqrt{\text{upper}}$; +$\sqrt{\text{upper}}$] iff 0 $\in$ A
- [-$\sqrt(\text{upper})$; - $\sqrt{\text{lower}}$] $\cup$ [$\sqrt{\text{lower}}$; $\sqrt{\text{upper}}$] if lower > 0
- $\emptyset$ else

**Division:**
$0 \not\in B$
- A*[$\frac{1}{\text{upper B}}$; $\frac{1}{\text{lower B}}$]

Division with $0 \in B$:


Next: Contraction
---
Goal: decide whether the box contains a common satisfying solution for all constraints

Solution: Contract the box without losing solutions

**Method 1**:
During contracting we might need to rearrange a constraint with regards to a variable so we *preprocess* it so that every constraint only contains either additions or multiplications. This might introduce new variables.

Choose a constraint c and x with $x \in c$

Evaluate one side and reduce the interval domain for x

**interval Newton method**

After proprocessing we have constraints $p = 0$ for polynomial $p$ and $x \sim 0$

Choose contration candidate $(c, x)$

Iff $c = x \sim 0$ do the first contraction
Else:
For univariate polynomial we can find a root by using the sequence $s_{i+1} = s_i - \frac{f(s_i)}{f'(s_i)}$, which converges to a root for "good enough" initial $s_0$

So we contract with $A := A \cap (s - \frac{f(s)}{f'(A)})$

Next: ICP Algorithm
---
- might not terminate

Keep track of Boxes

- Choose box
- if |box| < D: check for validity
- else contract or split
- again

Next: Contraction candidate choice
---
- best: relative gain(size old - size new / size old) is not predicable therefore not feasible
- solution: choose CC with highest weight, weight gets updated

Non-linear real arithmetic
---

- Interval constraint propagation
- Subtropical satisfiablility
- virtual substritution
- cylindrical algebraic decomposition

Subtropical satisfiability
---
- Not complete -> combine with complete method
- Either finds positive solution quickly or return unknown

Find solutions for $p > 0$ ($p < 0 \rightarrow -p > 0$)
For equalities $p = 0$:
- choose random point q
- if $p(q) = 0 \Rightarrow$ done
- else if $p(q) < 0$ search for any point $p(v) > 0$ then somewhere in between $p = 0$

For polynomials for every direction a polynomial is dominating therefore it's sign will determine the sign of the polynomial.
We want to satisfy $p > 0$ so we search for a direction where a positive monimial is dominating.

Separate moniomials into positive and negative frames $xy + x - xy^2 \Rightarrow \text{frame}_+ = \{(1,1), (1,0)\}; \text{frame}_- = \{(1, 2)\}$

**Newton Polytope:**
Convex hull of the frame of a hull. Convex hull is the smallest convex shape that includes all points of the frame.

**face(direction):**
A face in a direction are the furthermost points in that direction, A face with dimension 0 is called a vertex.

For every vertex on the polytope there exists a plane separating this vertex from all others.

This plane can be written as a vector in the direction (normalvector) of the separated vertex.

If you are a vertex on the polytope in the direction of the separating hyperplane the corresponding monomial is dominating.

We can find the normal vector by using a linear problem.

Next: Full Algorithm
---
- Given polynomial p
- setup frames
- get newton polytype
- check for existence of positive vertex
- find the normalvector for a separating hyperplane $n*v > b \land n*v' < b \forall \text{other} v'$
- choose a = 2
- check if polynome is positive for $a^n$ else double a and try again

Next: Finding root for $p(1,...,1) < 0 < p(v)$
---
We find $p = 0$ on a line between $(1, ...,1)$ and $v$

Then we construct $p(x_1, ..., x_n) \rightarrow p(1 + (v_{x_1} - 1)*t, ..., 1 + (v_{x_n} - 1)*t) = p^*(t)$
Solve for $p^*(t) = 0$
Recalculate values for the variables along the line with $1 + (v_{x_i} - 1)*t = x_i$.

Non-linear real arithmatic
---
- Equasions are sufficient ($p \geq 0 \Rightarrow \exists e p - e^2 = 0$)

Next: Removing FO-quantifiers
---
- Transform into pränex normalform
- Iteratively remove quantifiers (We can only remove existential quantors by negating universal quantors)

Problem: $\mathbb{R}$ is uncountably infinite
Idea: Find a finite set $T \subset \mathbb{R}$
T consists of one sample point from each sign-invariant region

For that we need to determine the real roots of polynomials

Virtual substitution
---
For existential real-algebraic formulas construct:
$\exists x_1... \exists x_n \varphi \equiv \exists x_1 ... \exists x_{n-1} \bigvee_{t \in T} \varphi[t//x_n]$

T contains test-candidates from each sign-invariant region.

We can construct a constraint to check for the existence of roots of polynomials of degree $\leq$ 2

From there we can create the relevant sign-invariant regions to check.

Next: The test candidates
---
For comparisions with equality:
- Each real root of p
- $- \infty$

For strict comparisons without equiality:
- Each real root of p $+ \varepsilon$
- $- \infty$

With multiple polynomials we use every test candidate from every constraint (see directly above).

Next: Substitution rules
---
Because we can't substitue $\infty$ for a variable we need rules to do so.

**Behold the comparision**

Cylindrical algebraic decompression (CAD)
---
- decomposes $\mathbb{R}^n$ into finitely many sign invariant regions
- select sample from every region
- check wether the constraints are satisfied by any example

Next: Interval representation
---
An interval represnetation of a root is $(p, i)$
- p is polynomial
- i is an _open_ interval
- there is exactly one real root of p in i

Next: Cauchy bound
---
For a real root $r$ of $p$

Cauchy bound is: $|r| \leq 1 + max\{\frac{\text{other coeficients}}{\text{leading coeficient}}\}$

This means all roots of a polynomial lie between $-C$ and $C$ ($C$ is the cauchy bound)

Next: Sturm Sequence
---
Sequence based on the ponyomial

Let $\sigma(x)$ is the number of sign changes in the sequence !0 is ignored and not counted as sign change!

Then the number of distinct roots of p in $(a, b]$ is $\sigma(a) - \sigma(b)$

Next: Full CAD Interval algorithm
---
Given polynomial constraints
- calculate cauchy bound
- compute each sturm sequence
- split each interval that contains
- more than one root of the same polynomial
- two different roots of two different polynomials

For every root interval:
- Split into intervals with:
CAD cells = $(-\infty, root_1), [root_1, root_1], (root_1, root_2), ..., [root_n, root_n], (root_n, \infty)$

Take a sample point from each CAD cell and test the constraints
for cells $[(p, i), (p, i)]$ the sign is 0
for cells $[(p_1, i_1), (p_2, i_2)]$ take a sample point p with $p > i_1$ and $p < i_2$