Symmetry in SAT: an overview

August 27th, 2018
Theory and Practice of SAT solving

Oaxaca, Mexico

Jo Devriendt, KU Leuven

Intro

Everyone knows symmetry:

"something does not change under a set of transformations"
- Wikipedia

Symmetry :=

Permutation of variable assignments that preserves satisfaction

In combinatorial solving

Symmetry induces symmetry classes:

Symmetry classes tend to get huge -> search problem

"......calculating......"

In combinatorial solving

Goal: investigate only asymmetrical cases

!!

Contents

1. Intro
2. SAT Prelims
3. "Classic" symmetry breaking
4. The pigeonhole problem
5. "Recent" symmetry breaking
6. Non-breaking approaches
7. Bonus: symmetry, local search & maxSAT

"Interesting research question"

In SAT:

Syntactic symmetry :=
literal permutation that preserves the CNF

a \vee \neg b \\ b \vee \neg c \\ c \vee \neg a
$a \vee \neg b \\ b \vee \neg c \\ c \vee \neg a$
a \mapsto b \\ \neg a \mapsto \neg b \\ b \mapsto c \\ \neg b \mapsto \neg c \\ c \mapsto a \\ \neg c \mapsto \neg a \\
$a \mapsto b \\ \neg a \mapsto \neg b \\ b \mapsto c \\ \neg b \mapsto \neg c \\ c \mapsto a \\ \neg c \mapsto \neg a \\$
(a\;b\;c)
$(a\;b\;c)$

static ↔ dynamic

other ↔ breaking

Shatter
BreakID

CDCLSym

SymChaff
Symmetric learning

?

Terminology

• variable x
• set of all variables X
• literal l
• clause c
• (propositional) formula φ
• (variable) assignment α
• α(l) is the truth value of l in α
• symmetry σ
• σ(...) is the symmetrical image of ...
• symmetry group Σ
• Σ(...) is the orbit of ... under Σ
• generator set gen(Σ)

Symmetry breaking formulas: Crawford [1]

Given: φ, Σ

Find: symmetry breaking formula sbf
that invalidates symmetrical assignments

\varphi
$\varphi$
\varphi \cup sbf
$\varphi \cup sbf$

Symmetry breaking formulas: Crawford [1]

Core idea: sbf encodes
"α is lexicographically smaller than σ(α)"
for σ ϵ Σ

x_1 \leq \sigma(x_1) \\ x_1 = \sigma(x_1) \Rightarrow x_2 \leq \sigma(x_2) \\ (x_1 = \sigma(x_1) \wedge x_2 = \sigma(x_2)) \Rightarrow x_3 \leq \sigma(x_3) \\ \ldots
$x_1 \leq \sigma(x_1) \\ x_1 = \sigma(x_1) \Rightarrow x_2 \leq \sigma(x_2) \\ (x_1 = \sigma(x_1) \wedge x_2 = \sigma(x_2)) \Rightarrow x_3 \leq \sigma(x_3) \\ \ldots$

parameter: total order on X

Symmetry breaking formulas: Crawford [1]

Sound

Complete

Huge: O(|X|²|Σ|)

Core idea: sbf encodes
"α is lexicographically smaller than σ(α)"
for all σ ϵ Σ

\varphi \cup sbf
$\varphi \cup sbf$

Symmetry breaking: Shatter [2]

• construct sbf for -much smaller- gen(Σ)
• "chain encoding"
• improved clausal encoding

Sound

Incomplete

Feasible: O(|X||gen(Σ)|)

\varphi \cup sbf
$\varphi \cup sbf$

Detecting symmetry: Saucy [3]

Sparse graph automorphism detection

• Graph construction from CNF:
• node for each literal and clause
• edge between literals occurring in clause
• edge between literal and negation
• No polynomial algorithm known
• Output: generators to automorphism group

Static symmetry breaking: Shatter+Saucy

Propositional description

off-the-shelf SAT solver

SAT/UNSAT

Graph automorphism detection

\neg a \vee b
$\neg a \vee b$

a \vee \neg b \\ b \vee \neg c \\ c \vee \neg a
$a \vee \neg b \\ b \vee \neg c \\ c \vee \neg a$
(a \; b \; c)
$(a \; b \; c)$

Pigeonhole!

Do n pigeons fit in n-1 holes?

• Proof-theoretic problem
• Simple but large symmetry group
• composition of "pigeon interchangeability"
and "hole interchangeability"
• 1 symmetry class
\forall p\colon \bigvee_{h} x_{ph} \\ \forall h\colon \forall p\neq p'\colon \neg x_{ph} \vee \neg x_{p'h}
$\forall p\colon \bigvee_{h} x_{ph} \\ \forall h\colon \forall p\neq p'\colon \neg x_{ph} \vee \neg x_{p'h}$
x_{11}
$x_{11}$
x_{21}
$x_{21}$
x_{31}
$x_{31}$
x_{41}
$x_{41}$
x_{12}
$x_{12}$
x_{22}
$x_{22}$
x_{32}
$x_{32}$
x_{42}
$x_{42}$
x_{13}
$x_{13}$
x_{23}
$x_{23}$
x_{33}
$x_{33}$
x_{43}
$x_{43}$

Pigeonhole!

Seems ok?

Original Shatter experiment:

Pigeonhole!

Modest gains...
Better results in original paper?

Own Shatter experiment:

Pigeonhole!

• Propositional encoding reduces "pigeon interchangeability"
to "row interchangeability"
• Shatter's sbf's are complete [4] with correct choice of
• gen(Σ)
• variable order

• |full sbf| = O(n²)
x_{11}
$x_{11}$
x_{21}
$x_{21}$
x_{31}
$x_{31}$
x_{41}
$x_{41}$
x_{12}
$x_{12}$
x_{22}
$x_{22}$
x_{32}
$x_{32}$
x_{42}
$x_{42}$
x_{13}
$x_{13}$
x_{23}
$x_{23}$
x_{33}
$x_{33}$
x_{43}
$x_{43}$

Pigeonhole!

x_{11}
$x_{11}$
x_{21}
$x_{21}$
x_{31}
$x_{31}$
x_{41}
$x_{41}$
x_{12}
$x_{12}$
x_{22}
$x_{22}$
x_{32}
$x_{32}$
x_{42}
$x_{42}$
x_{13}
$x_{13}$
x_{23}
$x_{23}$
x_{33}
$x_{33}$
x_{43}
$x_{43}$
• Propositional encoding reduces "pigeon interchangeability"
to "row interchangeability"
• Shatter's sbf's are complete [4] with correct choice of
• gen(Σ)
• variable order

• |full sbf| = O(n²)

Symmetry breaking: BreakID [5]

Core idea: detect "row swap" symmetries

1. Search σ1 , σ2 ϵgen(Σ) that form 2 subsequent row swaps
• forms initial 3-rowed variable matrix M
2. Apply every σ ϵ gen(Σ) to all detected rows r ϵ M so far
• images σ(r) disjoint of M are candidates to extend M
• test if swap r ↔ σ(r) is a symmetry by syntactical check on φ
• if success, extend M with σ(r)
3. Use Saucy to extend gen(Σ) with new symmetry generators by fixing all variable nodes with variable in M, first row excepted

*Approximative algorithm

Symmetry breaking: BreakID [5]

Core idea: detect "row swap" symmetries

Detect row interchangeability subgroups?

Caveat!

\neg x_1 \vee \sigma(x_1)
$\neg x_1 \vee \sigma(x_1)$
• First clause in sbf for σ is binary:

• x is stabilized by Σ iff Σ(x)={x}
• Given Σ with smallest non-stabilized x, for each x' ϵ Σ(x):

is clause of sbf under some σ ϵ Σ
\neg x \vee x'
$\neg x \vee x'$

Symmetry breaking: BreakID [5]

Core idea: maximize number of binary sbf clauses

• Create stabilizer chain of Σ:

• Σi is the stabilizer subgroup of Σi-1 stabilizing the next non-stabilized variable in ordering
• Σi have different smallest non-stabilized variables xi
• For each x' ϵ Σi(xi)

is a clause of some sbf
\Sigma \supset \Sigma_1 \supset \Sigma_2 \supset \ldots \supset 1
$\Sigma \supset \Sigma_1 \supset \Sigma_2 \supset \ldots \supset 1$
\neg x_i \vee x'
$\neg x_i \vee x'$

Symmetry breaking: BreakID [5]

Core idea: exploit binary sbf clauses

\sigma(x)=\neg x
$\sigma(x)=\neg x$

Symmetry breaking: BreakID [5]

Core idea: exploit binary sbf clauses

• Approximative implementation
• which adapts the variable order!

• Works well for polarity symmetry σ where for all x:

as sbf is equivalent to unit clause

and their number is maximized through adopted variable order.
\neg x_1
$\neg x_1$

Complete algorithm?

Symmetry breaking: CDCLSym [6]

Core idea: generate sbf dynamically

• Keep track of reducer symmetries where σ(α)<α
• by watching smallest variable s.t. σ(v)≠v
• Generate clause from sbf forcing α≤σ(α)

Use clauses for propagation?

Not only generator symmetries?

Symmetry breaking: On completeness

• Pigeon interchangeability can be completely broken with polynomial sbf
• E.g., find coloring of complete graph (Ramsey numbers)
• Recent intrest [11] [14]
• How about general interchangeability over arbitrary high dimensional relations?

Tractable sbf for edge interchangeability?

Symmetry breaking: Prefix breaking [7]

Core idea: enumerate asymmetrical assignments to variable prefix

High-level constraints

Incremental / parallel SAT solver

Graph  representation

\forall x\colon \exists y\colon \\ \varphi(x,y)
$\forall x\colon \exists y\colon \\ \varphi(x,y)$

Symmetry class representative enumeration

Variable prefix

Clausal encoding

Symmetry handling: SymChaff [8]

Core idea: search decisions consider row interchangeability

x_{11}
$x_{11}$
x_{21}
$x_{21}$
x_{31}
$x_{31}$
x_{41}
$x_{41}$
x_{12}
$x_{12}$
x_{22}
$x_{22}$
x_{32}
$x_{32}$
x_{42}
$x_{42}$
x_{13}
$x_{13}$
x_{23}
$x_{23}$
x_{33}
$x_{33}$
x_{43}
$x_{43}$
• Only for row interchangeability symmetry
• Keep track of row-interchangeable variables
• interchangeability reduces under previous choices
• Use cardinality decision points over row-interchangeable variables

Cardinality decision of 1 over first column:

Symmetry handling: SymChaff [8]

• Only for row interchangeability symmetry
• Keep track of row-interchangeable variables
• interchangeability reduces under previous choices
• Use cardinality decision points over row-interchangeable variables

Core idea: search decisions consider row interchangeability

0
$0$
0
$0$
0
$0$
1
$1$
x_{12}
$x_{12}$
x_{22}
$x_{22}$
x_{32}
$x_{32}$
x_{42}
$x_{42}$
x_{13}
$x_{13}$
x_{23}
$x_{23}$
x_{33}
$x_{33}$
x_{43}
$x_{43}$

Cardinality decision of 1 over first column:

Symmetry handling: SymChaff [8]

Strong performance on pigeonhole

Symmetry handling: Symmetric learning [9]

• Learnt clauses are logical consequences of φ
• Whenever c is a consequence of φ, so is σ(c)
• Problem: Σ(c) is huge
• Learn only σ(c) for σ ϵ gen(Σ)

Core idea: consider symmetrical learned clauses

Symmetry handling: Symmetric explanation learning [10]

• Learn σ(c) that propagate at least once
• symmetries typically permute only a fraction of the literals
• if c is unit, σ(c) has a good chance of being unit as well
• explanation clauses are unit ;-)

Core idea: consider useful symmetrical explanation clauses

• For each σ ϵ gen(Σ), whenever c propagates, store σ(c) in a separate clause store θ
• Propagation on θ happens only if standard unit propagation is at a fixpoint
• Whenever a σ(c) ϵ θ propagates, upgrade it to a "normal" learned clause
• After backjump over c's propagation level, clear σ(c) from θ
• Every learned σ(c) is useful & original
• Transitive effect: track σ'(σ(c)) when σ(c) propagates

Symmetry handling: Symmetric explanation learning [10]

Core idea: consider useful symmetrical explanation clauses

Symmetry handling: Symmetric explanation learning [10]

What is "complete" symmetrical learning?

Can it be done efficiently?

Caveat: performance on larger instances

Research trends:

• Symmetry detection on propositional level is hard
• not a solved problem, cfr. pigeonhole
• papers often assume high-level symmetry input [7] [8]
• Sbf construction based on canonical labeling [7] [11]
• Dynamical approaches often perform lazy clause generation [6] [10] [12]
• Use computational group algebra to detect symmetry group structure [5] [13]

The influence of the variable order on an sbf?

Proof checking and symmetrical learning?

Thanks for listening! Questions?

[1] Symmetry-Breaking Predicates for Search Problems (1996) Crawford et al.

[2] Efficient Symmetry-Breaking for Boolean Satisfiability (2003) Aloul et al.

[3] Symmetry and Satisfiability: An Update (2010) Katebi et al.

[4] Breaking row and column symmetries in matrix models (2002) Flener et al.

[5] Improved Static Symmetry Breaking for SAT (2016) Devriendt et al.

[6] CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving (2018) Metin et al.

[7] An Adaptive Prefix-Assignment Technique for Symmetry Reduction (2017) Juntilla et al.

[8] Symchaff: exploiting symmetry in a structure-aware satisfiability solver (2009) Sabharwal

[9] Enhancing clause learning by symmetry in SAT solvers (2010) Benhamou

[10] Symmetric explanation learning: Effective dynamic symmetry handling for SAT (2017) Devriendt et al.

[11] Breaking Symmetries in Graphs: The Nauty Way (2016) Codish et al.

[12] Symmetries, almost symmetries, and lazy clause generation (2014) Chu et al.

[13] Breaking symmetries in all-different problems (2005) Puget

[14] The quest for perfect and compact symmetry breaking for graph problems (2016) Heule

Bonus: symmetry, local search & maxSAT

• (Satisfying) assignments now have an associated score
• Local search "moves" from one to the other based on structure-preserving transformations

Bonus: symmetry, local search & maxSAT

• (Satisfying) assignments now have an associated score
• Local search "moves" from one to the other based on structure-preserving transformations
• Designing local moves is typically done by hand...

Bonus: symmetry, local search & maxSAT

• (Satisfying) assignments now have an associated score
• Local search "moves" from one to the other based on structure-preserving transformations
• Designing local moves is typically done by hand...

Symmetries form moves!
Can be automatically detected!

Bonus: symmetry, local search & maxSAT

Symmetry-based local search in weighted maxSAT?

By krr

Copy of Symmetry in SAT: an overview

talk for Theory and Practice of Satisfiability Solving

• 145
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 79, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}