Boolean SAT(isfiability)
and Optimisation

Charles Gretton

https://charlesgretton.github.io/2024symposium/optimal.html

Why are we learning about the SAT decision problem?

AI Planning is solved OPTIMALLY using SAT

Optimisation is how SAT can be solved$\ldots$

What's the (SAT) problem?!

Propositional Logic

Alphabet of propositions $\cal P$

$\cal P$ is finite set $\{p, q, r, \ldots\}$
e.g. let $p=$"Charles is talking now"

$p \in {\cal P}$ is called an atomic expression
Terms $x,y, \ldots$ can be general expressions
Expressions via binary infix connectives:
And otherwise our unary prefix connective:

Modelling Relation $\models$ called "Double Turnstile"

Let $\alpha$ be an truth assignment for ${\cal P}$
We write $\alpha \models x$ if $\alpha$ satisfies expression $x$

$\begin{array}{rllcl} \alpha & \models p & \text{iff} & \alpha(p)=\top\\ \alpha & \models \lnot x & \text{iff} & \alpha \not\models x \\ \alpha & \models x \land y & \text{iff} & \alpha \models x \; \text{and} \; \alpha \models y \\ \alpha & \models x \lor y & \text{iff} & \alpha \models x \; \text{or} \; \alpha \models y \\ \alpha & \models x \to y & \text{iff} & \alpha \not\models x \; \text{or} \; \alpha \models y \\ \end{array} $ Language with $\{\land, \lor, \lnot\}$ is complete for Boolean functions

The Boolean SAT(isfiability) Problem

Given expression $x$ determine if $\exists \alpha$ s.t. $\alpha \models x$

A literal is a proposition $p$ or its negation $\overline{p}$

A disjunctive clause is a disjunction over literals - e.g. $(p_1 \lor \overline{p_3} \; )$

Conjunctive Normal Form (CNF) expression is conjunction of disjunctive clauses:

DIMACS CNF	Interpretation/Expression
`p cnf 3 2 1 -3 0 2 3 -1 0`	$\begin{array}{l} \text{CNF problem with 3 propositions and 2 disjunctive clauses}\\ (p_1 \lor \overline{p_3} \; ) \\ \land (p_2 \lor p_3 \lor \overline{p_1} \;) \end{array}$

How do you solve it?!

The Boolean SAT(isfiability) Problem

${NP}$-complete - Generally below approaches have exponential worst case runtime

Approach	Optimisation	Complete	Syntactic	Gist
Resolution	✘	✓	✓	Inference
SLS	✓	✘$^1$	✘	Local Search
DPLL	✘	✓	✘	Systematic Search
CDCL	✘	✓	✘	DPLL with Inference

¹some exhibit approximately complete behaviour

How do you resolve?!

J. A. Robinson 1965

Year "Satisfaction" was recorded by Otis Redding...

Resolution - Rule of Inference

The Rule:

$\begin{array}{c} \text{premise, admits resolving on}\;p \\ \hline \textsf{resolvant}\; \text{is a new disjunctive clause} \end{array}$

Example:

$\begin{array}{c} (x \lor p) \land (\overline{p} \lor y) \\ \hline (x \lor y) \end{array}$

Resolution - Refutation Proof

Proof of $\nexists \alpha$ s.t. $\alpha \models x$

$\circ$ Let $x$ be a CNF; Write $c_i\in x$ for clause $c_i$ in $x$
$\circ$ $c\land c'\vdash_R c_R$ says $c_R$ is a resolvant of $c$ and $c'$
$\circ$ $\pi = \langle c_1,c_2, ..., c_m \rangle$ is a resolution refutation
$\;\; \circ$ $c_i\in x$ or $c_j\land c_k\vdash_R c_i$ where $j,k < i$
$\;\; \circ$ $c_m=\{\}$, contains no literals, is unsatisfiable

Resolution of $\text{PHP}^3_2$

The Problem - $\text{PHP}^3_2$

c1$\begin{array}{c:c:c} \blacksquare & & \\ \hdashline \blacksquare & & \\ \end{array}$ c2$\begin{array}{c:c:c} & \blacksquare & \\ \hdashline & \blacksquare & \\ \end{array}$ c3$\begin{array}{c:c:c} & & \blacksquare \\ \hdashline & & \blacksquare \\ \end{array}$

c4$\begin{array}{c:c:c} \square & \square & \\ \hdashline & & \\ \end{array}$ c5$\begin{array}{c:c:c} \square & & \square \\ \hdashline & & \\ \end{array}$ c6$\begin{array}{c:c:c} & \square & \square \\ \hdashline & & \\ \end{array}$

c7$\begin{array}{c:c:c} & & \\ \hdashline \square & \square & \\ \end{array}$ c8$\begin{array}{c:c:c} & & \\ \hdashline \square & & \square \\ \end{array}$ c9$\begin{array}{c:c:c} & & \\ \hdashline & \square & \square \\ \end{array}$

$L_1$ - Resolvants - $\text{PHP}^3_2$

c14$\begin{array}{c:c:c} & \square & \\ \hdashline \blacksquare & & \\ \end{array}$ c15$\begin{array}{c:c:c} & & \square \\ \hdashline \blacksquare & & \\ \end{array}$ c17$\begin{array}{c:c:c} \blacksquare & & \\ \hdashline & \square & \\ \end{array}$

c18$\begin{array}{c:c:c} \blacksquare & & \\ \hdashline & & \square \\ \end{array}$ c24$\begin{array}{c:c:c} \square & & \\ \hdashline & \blacksquare & \\ \end{array}$ c26$\begin{array}{c:c:c} & & \square \\ \hdashline & \blacksquare & \\ \end{array}$

c27$\begin{array}{c:c:c} & \blacksquare & \\ \hdashline \square & & \\ \end{array}$ c29$\begin{array}{c:c:c} & \blacksquare & \\ \hdashline & & \square \\ \end{array}$ c35$\begin{array}{c:c:c} \square & & \\ \hdashline & & \blacksquare \\ \end{array}$

$L_1$ - Resolvants - $\text{PHP}^3_2$

c36$\begin{array}{c:c:c} & \square & \\ \hdashline & & \blacksquare \\ \end{array}$ c38$\begin{array}{c:c:c} & & \blacksquare \\ \hdashline \square & & \\ \end{array}$ c39$\begin{array}{c:c:c} & & \blacksquare\\ \hdashline & \square & \\ \end{array}$

$L_2$ - Resolvants - $\text{PHP}^3_2$

$\begin{array}{c:c:c} & & \\ \hdashline & \square & \blacksquare \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline \blacksquare & & \square \\ \end{array}$ $\begin{array}{c:c:c} & \blacksquare & \square \\ \hdashline & & \\ \end{array}$

$\begin{array}{c:c:c} & \square & \blacksquare \\ \hdashline & & \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline \square & \blacksquare & \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline & \blacksquare & \square \\ \end{array}$

$\begin{array}{c:c:c} & & \\ \hdashline \blacksquare & \square & \\ \end{array}$ $\begin{array}{c:c:c} \square & \blacksquare & \\ \hdashline & & \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline \square & & \blacksquare \\ \end{array}$

$L_2$ - Resolvants - $\text{PHP}^3_2$

$\begin{array}{c:c:c} \blacksquare & \square & \\ \hdashline & & \\ \end{array}$ $\begin{array}{c:c:c} \square & & \blacksquare \\ \hdashline & & \\ \end{array}$ $\begin{array}{c:c:c} \blacksquare & & \square \\ \hdashline & & \\ \end{array}$

$L_3+$ - The Proof - $\text{PHP}^3_2$

$\begin{array}{c:c:c} \color{red}{\blacksquare} & & \\ \hdashline & \color{red}{\square} & \\ \end{array}$ $\begin{array}{c:c:c} \color{red}{\square} & & \\ \hdashline & & \color{red}{\blacksquare} \\ \end{array}$ $\vdash_R \begin{array}{c:c:c} & & \\ \hdashline & \color{red}{\square} & \color{red}{\blacksquare} \\ \end{array}$

$\begin{array}{c:c:c} & & \color{red}{\square} \\ \hdashline & \color{red}{\blacksquare} & \\ \end{array}$ $\vdash_R \begin{array}{c:c:c} & & \square \\ \hdashline & & \blacksquare \\ \end{array}$ $\begin{array}{c:c:c} & & \color{red}{\blacksquare} \\ \hdashline & & \color{red}{\blacksquare} \\ \end{array}$

$\vdash_R \begin{array}{c:c:c} & & \\ \hdashline & & \blacksquare \\ \end{array}$ $\begin{array}{ccc} \centerdot & \centerdot & \centerdot \\ \end{array}$ $\vdash_R \begin{array}{c:c:c} & & \\ \hdashline & \blacksquare & \\ \end{array}$

$L_3+$ - Finally - $\text{PHP}^3_2$

$\begin{array}{c:c:c} & & \\ \hdashline & & \color{red}{\blacksquare} \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline & \color{red}{\blacksquare} & \\ \end{array}$ $\begin{array}{c:c:c} & & \\ \hdashline & \color{red}{\square} & \color{red}{\square} \\ \end{array}$

$\vdash_R \begin{array}{c:c:c} & & \\ \hdashline & & \square \\ \end{array}$ $\vdash_R \begin{array}{c:c:c} & & \\ \hdashline & & \\ \end{array}$ $\begin{array}{ccc} Q. & E. & D. \\ \end{array}$

Backtracking

DPLL: Search with Unit Propagation

$\{$Davis$^{*\dagger}$,Putnam$^*$,Logemann$^\dagger$,Loveland$^\dagger$$\}$
$\{$1960$^{*}$,1962$^{\dagger}$$\}$

Concept of Unit Propagation (UP)

$\circ$ Let $x$ be a CNF and $\ell$ a literal
$\circ$ We define $x\downharpoonright\ell=x'$
$\;\; \circ$ $\forall c\in x$ s.t. $\{\ell, \overline{\ell}\} \cap c \equiv \emptyset$ we have $c\in x'$
$\;\; \circ$ $\forall c\in x$ s.t. $\ell \in c$ we have $c\not\in x'$
$\;\; \circ$ $\forall c\in x$ s.t. $\overline{\ell} \in c$ we have $c \backslash \overline{\ell} \in x'$
$\;\; \circ$ $x'$ only contains the inclusions above

$\circ$ Denoted ${UP}(x)$, iteratively until fixpoint:
$\;\; \circ$ For unit $\{\ell\}\in x$ apply $x\downharpoonright\ell$

DPLL


		bool DPLL(set:Clause x)
		  // Simplify formula with Unit Propagation
		  x=UP(x); 
		  while ( p <- x && pure(x,p) )
	            // i.e. All occurences of p in x have same parity
		    x=UP(x /\ {sign(p,x)p});
		  // Occurrences of each proposition have same parity
    if (consistent_set(x)) return true; // SAT
		  // Empty disjunctive clause cannot be satisfied
		  if ( c <- x && |c| == 0 ) return false ; // UNSAT
		  // i.e. proposition selection heuristic
		  p=select_proposition(x);
		  return DPLL(x /\ {p}) || DPLL(x /\ {-p});

DPLL and tree-like resolution are polynomially equivalent (i.e. at refutation)

Have you learnt nothing?!

the naughties -
lifelong learning and microcredentials

CDCL


bool CDCL(set:Clause x,list:Literal D=[], set:Clause LC={})
do{
  if ( {} <- UP(D /\ LC /\ x) ){
    if ( D == [] ) return false; // UNSATISFIABLE
    c = CONFLICT (D /\ LC /\ x);
    m = assertion_level(c, D);
    D = D[:m];
    LC = c /\ LC;
  } else {
    if ( RESTART ) D=[];
    l=select_literal(D /\ LC /\ x);
    if ( NULL == l ) return true; // SATISFIABLE
    D=D+[l]
  }
}while(true);

CDCL polynomially simulates general resolution (i.e. at refutation)

Are there degrees of satisfaction?

Yes, lots of them$\ldots$

as explored by
Stochastic Local Search (SLS)

SAT as Optimisation

Let $\alpha$ be an assignment to all propositions in $x$

\[\mathbf{f}(\alpha,c) = \bigg\{ \begin{array}{ccc} 0 & \text{if} & \alpha\models c\\ 1 & \text{if} & \alpha\not\models c \end{array} \]

\[\mathbf{V}_x(\alpha) = \sum_{c\in x} \mathbf{f}(\alpha,c) \]

Objective is to minimise unsatisfied clauses

SAT as Optimisation - The Approach

Initially: $\alpha$ is arbitrary
Flip the parity of one truth assignment in $\alpha$
Continue to flip greedily until $\mathbf{V}_x(\alpha)=0$

Or heat death of the universe $\ldots$

Is there any SAT software to play with?

Dagster - A Hybrid HPC SAT Solver

Communicating CDCL and SLS processes
Scheduled parallel solving of subproblems
Solutions communicated with orchestrator
Designed for difficult and/or big problems
Learn more from our tutorials

What is (Theoretically) More Powerful?

Cutting Planes Proofs!

Exposition here follows that of M. Vinyals, 2016

Cutting Planes Proofs - $a,b,c$ are scalars

Axioms
$\frac{}{p\geq 0} \;\; \frac{}{-p \geq -1}\\$
The Addition Rule
$\frac{\sum a_i p_i \geq a \;\; \sum b_i p_i \geq b}{\sum (a_i + b_i)p_i \geq a + b}\\$
The Division Rule -- i.e., $ \lceil p \rceil$, 'ceiling', rounds up
$\frac{\sum a_i p_i \geq a}{\sum (a_i / c) p_i \geq \lceil a/c \rceil }\\$
Sequential proof seeks: $0 \geq 1$

PHP Example

$p_{ij}$ if pigeon $i$ occupies hole $j$
Derive: $\sum_{i=1}^{n+1} p_{ij} \leq 1$, equiv. $\sum_{i=1}^{n+1} - p_{ij} \geq -1$
${\small -p_{11} - p_{21} \geq -1 \;\; -p_{11} - p_{31} \geq -1 \;\; -p_{21} - p_{31} \geq -1 } $
$-2p_{11} - 2p_{21} - 2p_{31} \geq -3$

$-p_{11} - p_{21} - p_{31} \geq -1$
Proof is available as:
$\{\sum_{j=1}^{n} p_{ij} \geq 1 \}_{i=1}^{n+1} \;\; \{\sum_{i=1}^{n+1} -p_{ij} \geq -1 \}_{j=1}^{n}$

$0 \geq 1$

Pseudo-Boolean Optimisation by Example

An Asset Mix and Assignment Problem

Notation and Propositions

Tasks: $f, g$; Asset: $a$; Asset Type:t

$V_a$ :: asset $a$ is used
$P_{fg}$ :: task $f$ precedes task $g$ on some asset
$P_{af}$ :: schedule for asset $a$ starts at task $f$
$D_f$ :: task f is scheduled
$D_fV_a$ :: task $f$ is scheduled on asset $a$
$T_{tf}$ :: task $f$ is serviced with an asset of type $t$
$C_{fgt}$ :: profit scheduling $f$ and $g$ on asset type $t$
$C_{aft}$ :: profit for asset $a$ of type $t$ starting at $f$

Constraints

$\sum_{f}P_{af}-V_{a}=0$ :: asset used iff scheduled
$\sum_{f}-P_{af}\geq -1$ :: assets starts once
$-D_{f} + \sum_{v}P_{vf} = 0$ :: task once as a successor
$-D_{f} + \sum_{a}D_{f}V_{a} = 0$ :: task assigned once
$-D_{f} + \sum_{g}-P_{fg} \geq 0$ :: task once as predecessor
$-P_{fg} + D_{f} \geq 0$; $-P_{fg} + D_{g}\geq 0$
$f$ scheduled with $g$, then its scheduled.
$-P_{fg} - D_{g}V_{a} + D_{f}V_{a} \geq -1 $;
$f$ scheduled with $g$ are served by one $a$

More Constraints and Objective

$-T_{tf} + \sum_{a:[t(a)=t]}(D_{f}V_{a}) = 0$
$f$ served by one $a$ of type $t$
$ - T_{tg} - P_{fg} + C_{fgt} \geq -1 $ ; $P_{fg} - C_{fgt} >= 0$
To incur a profit $C_{fgt}$

Objective

$\min\sum_{vgt}( -\$_{vgt} C_{vgt})$

Find Smallest Ramsey Coloring

Consider undirected cliques
A Ramsey Coloring Satisfies:

There are no monochromatic triangles.
Every non-monochromatic triangle appears everywhere it can.

Problem: Find a smallest Ramsey coloring.

Get Dagster - A SAT and #SAT Solver


		  git clone git@github.com:ANU-HPC/dagster.git

(Optional) Build a Container

...this will take time...


		 docker build --no-cache -t milthorpe/async-neighbours .

(Optional) Run the Container you Built


		  docker run -it --mount src=`pwd`,target=/home/appuser,\
		                    type=bind milthorpe/async-neighbours

Build Dagster SAT and #SAT Solver


		  cd dagster
		  make -j 16
		  cd .. # Back to the root folder

Build Relaxed Coloring Problem Generator

There are no monochromatic triangles.
Every non-monochromatic triangle appears at every vertex.


		  cd Benchmarks/ramsey
		  make

Make 2-Color Problems for Cliques of size N=4,..,10

The 'map' file is interpretation of propositions
The 'cnf' file is problem clauses/constraints
ALERT: some symmetry breaking


		  for i in {4..10} ; do
		      ./generate_ramsey_NM -N $i -M 2 2> ramsey.M2.N$i.map
		                                       > ramsey.M2.N$i.cnf 
		      mv dag_${i}_2.dag ramsey.M2.N$i.dag
		  done
		  cd ../../ # Back to the root folder

Find Cliques with SAT Solver


		  cd dagster
		  for i in {4..10} ; do echo $i ;
		      mpirun -n 4 ./dagster -m 0 -e 1 \
		             ../Benchmarks/ramsey/ramsey.M2.N$i.dag \
		             ../Benchmarks/ramsey/ramsey.M2.N$i.cnf
		      if [ $(cat dag_out.txt | wc -l) -gt 0 ] ; then
		          mv dag_out.txt ramsey.M2.N$i.sol
		      fi
		  done

Take Inventory of the Outputs


		  ls ramsey.*


		  ramsey.M2.N4.sol  ramsey.M2.N5.sol

Look at Smallest Candidate - Is this Ramsey?


		  for f in `cat ramsey.M2.N4.sol | tr ' ' '\n' | grep -v ^-` ; do
		      cat ../Benchmarks/ramsey/ramsey.M2.N4.map | grep :\ $f\ -
		  done


		  MAPPING: 2 -> v2 x v3 = c1
		  MAPPING: 4 -> v1 x v3 = c1
		  MAPPING: 5 -> v0 x v3 = c0
		  MAPPING: 7 -> v1 x v2 = c0
		  MAPPING: 10 -> v0 x v2 = c1
		  MAPPING: 11 -> v0 x v1 = c0

Look at Other Candidate - Is this Ramsey?


		  for f in `cat ramsey.M2.N5.sol | tr ' ' '\n' | grep -v ^-` ; do
		      cat ../Benchmarks/ramsey/ramsey.M2.N5.map | grep :\ $f\ -
		  done


		  MAPPING: 2 -> v3 x v4 = c1
		  MAPPING: 4 -> v2 x v4 = c1
		  MAPPING: 5 -> v1 x v4 = c0
		  MAPPING: 7 -> v0 x v4 = c0
		  MAPPING: 9 -> v2 x v3 = c0
		  MAPPING: 12 -> v1 x v3 = c1
		  MAPPING: 13 -> v0 x v3 = c0
		  MAPPING: 15 -> v1 x v2 = c0
		  MAPPING: 18 -> v0 x v2 = c1
		  MAPPING: 20 -> v0 x v1 = c1

Keep learning!

$\rightarrow\star$Co-Lab Honours Grant$\star\leftarrow$
$\rightarrow\star$Apply ASAP for PhD @ ANU$\star\leftarrow$
$\rightarrow\star$CSIRO ($\psi\rho$) AI4Missions$\star\leftarrow$
$\rightarrow\star$Data61 PhD$\star\leftarrow$
$\rightarrow\star$$\psi\rho$ Next Generation Graduates Program$\star\leftarrow$

Approach	Optimisation	Complete	Syntactic	Gist
Resolution	✘	✓	✓	Inference
SLS	✓	✘\(^1\)	✘	Local Search
DPLL	✘	✓	✘	Systematic Search
CDCL	✘	✓	✘	DPLL with Inference

Boolean SAT(isfiability) and Optimisation

https://charlesgretton.github.io/2024symposium/optimal.html

Why are we learning about the SAT decision problem?

What's the (SAT) problem?!

Propositional Logic

Modelling Relation \(\models\) called "Double Turnstile"

The Boolean SAT(isfiability) Problem

How do you solve it?!

The Boolean SAT(isfiability) Problem

How do you resolve?!

J. A. Robinson 1965

Year "Satisfaction" was recorded by Otis Redding...

Resolution - Rule of Inference

Resolution - Refutation Proof

Resolution of \(\text{PHP}^3_2\)

The Problem - \(\text{PHP}^3_2\)

\(L_1\) - Resolvants - \(\text{PHP}^3_2\)

\(L_1\) - Resolvants - \(\text{PHP}^3_2\)

\(L_2\) - Resolvants - \(\text{PHP}^3_2\)

\(L_2\) - Resolvants - \(\text{PHP}^3_2\)

\(L_3+\) - The Proof - \(\text{PHP}^3_2\)

\(L_3+\) - Finally - \(\text{PHP}^3_2\)

Backtracking

DPLL: Search with Unit Propagation

Concept of Unit Propagation (UP)

DPLL

Have you learnt nothing?!

the naughties - lifelong learning and microcredentials

CDCL

Are there degrees of satisfaction?

Yes, lots of them\(\ldots\)

as explored by Stochastic Local Search (SLS)

SAT as Optimisation

SAT as Optimisation - The Approach

Is there any SAT software to play with?

Dagster - A Hybrid HPC SAT Solver

What is (Theoretically) More Powerful?

Cutting Planes Proofs!

Exposition here follows that of M. Vinyals, 2016

Cutting Planes Proofs - \(a,b,c\) are scalars

PHP Example

Pseudo-Boolean Optimisation by Example

An Asset Mix and Assignment Problem

Notation and Propositions

Constraints

More Constraints and Objective

Objective

Find Smallest Ramsey Coloring

Get Dagster - A SAT and #SAT Solver

(Optional) Build a Container

...this will take time...

(Optional) Run the Container you Built

Build Dagster SAT and #SAT Solver

Build Relaxed Coloring Problem Generator

Make 2-Color Problems for Cliques of size N=4,..,10

Find Cliques with SAT Solver

Take Inventory of the Outputs

Look at Smallest Candidate - Is this Ramsey?

Look at Other Candidate - Is this Ramsey?

Keep learning!

Questions??

Boolean SAT(isfiability)
and Optimisation

the naughties -
lifelong learning and microcredentials

as explored by
Stochastic Local Search (SLS)