JavaScript isn't enabled in your browser, so this file can't be opened. Enable and reload.

1 of 40

CDCL SAT Solving and �Applications to Optimization Problems

Alexander Nadel, Intel & Technion, Israel

February 18, 2024

Technion, Haifa, Israel�

Up-to-date version of a talk first given at �Satisfiability: Theory, Practice, and Beyond Workshop, Simons Institute, UC Berkeley, USA on April 17, 2023�Video Recording of the 2023 Talk @ Berkeley

PEG PDS DDI

1/11

The ability of modern SAT solvers to handle huge industrial instances is highly intriguing, if not mysterious. It is well-known that the breakthrough in capacity was enabled by the introduction of the so-called Conflict-Driven-Clause-Learning (CDCL) solvers in the late 90s and early 00s. In the first part of this talk, we review CDCL fundamentals, including the seminal works on the first CDCL solvers GRASP and Chaff, Boolean Constraint Propagation (BCP) algorithm and later works on chronological backtracking. The second part of our talk is about applying SAT to solving optimization problems. Specifically, we review the Polosat algorithm to optimize a user-given black-box function, given a SAT formula. Polosat enabled a breakthrough in the capacity of our industrial tool for cell placement in physical design, and it also serves as an essential component of modern anytime MaxSAT solvers (such as the winner of the latest MaxSAT Evaluation 2022 in all the incomplete categories NuWLS-c).

2 of 40

Agenda

Core CDCL SAT Solving

Review of the foundations

Solving Complex Optimization Problems with SAT

Opportunity for the future

based on my own industrial experience

PEG PDS DDI

2/11

3 of 40

Introduction

SAT: determine if a Boolean formula in Conjunctive Normal Form (CNF) satisfiable

The original NP-Complete problem: the famous Cook-Levin theorem (early 70s)

SAT has exponential complexity unless P = NP -- whether or not P = NP is frequently called the most important outstanding question in CS

Check a solution is easy 🡪 is it also easy to solve?
One of the 7 Clay Millennium Prize Problems – worth $1,000,000

SAT is an unresolved mystery

Yet, SAT solvers are scalable widely used tools, how come?!

2/18/2024

F = (a ∨ b) ∧ (¬a ∨ ¬b ∨ c)

clause #1

clause #2

Literals

PEG PDS DDI

3/11

4 of 40

SAT Fundamentals: Backtrack Search

The baseline algorithm in modern SAT solvers is backtrack search

Called DPLL or DLL

Davis, Martin; Logemann, George; Loveland, Donald: "A Machine Program for Theorem Proving". Communications of the ACM. 5 (7): 394–397. (1961).

Davis, Martin; Putnam, Hilary: A computing procedure for quantification theory. Journal of the ACM 7 (1960)

2/18/2024

PEG PDS DDI

4/11

5 of 40

From Enumeration to DPLL

2/18/2024

Apply the unit clause rule till fixed-point aka Boolean Constraint Propagation (BCP)

Carry out backtrack search.

Stop when a model is found

The unassigned literal c₁must be implied

F = (a ∨ b) ∧ (¬a ∨ ¬b ∨ c)

clause #1

clause #2

Literals

Stop when a clause turns UNSAT

c₂

c₁

c₃

c₂

c₁

c₃

Falsified literal:

Satisfied literal:

Unassigned literal:

A unit clause -- one unassigned, rest falsified:

The unit clause rule: the unassigned literal in a unit clause must be 1

Implied in parent clause #1:

PEG PDS DDI

5/11

6 of 40

The Mystery of SAT Solver Scalability

DPLL could handle formulas with <2,000 clauses

Modern SAT solvers cope with industrial instances of 100,000,000’s clauses

The introduction of Conflict-Driven-Clause-Learning (CDCL) or, simply, �Conflict-driven Solving was the birth of modern highly-scalable SAT solving

Learn from conflicts to drive & prune backtrack search

2/18/2024

PEG PDS DDI

6/11

7 of 40

CDCL: the Intuitive Principles

Learning and pruning

Block already explored sub-spaces

Locality

Focus the search on the relevant data
Learn strong clauses from the local context

Well-engineered data structures

Extremely fast Boolean Constraint Propagation (BCP)

Beyond CDCL

Inprocessing
Local search integration

2/18/2024

PEG PDS DDI

7/11

8 of 40

Today’s Focus for the 1^st Part of the Talk

In-depth dive into the “core of the core”

Conflict analysis loop
Boolean Constraint Propagation (BCP)

PEG PDS DDI

8/11

9 of 40

Conflict-driven SAT Solving: Seminal Work

1996: GRASP by Joao P. Marques-Silva and Karem A. Sakallah

João P. Marques Silva, Karem A. Sakallah: GRASP - a new search algorithm for satisfiability. ICCAD 1996: 220-227��2001: Chaff by Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik

Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver. DAC 2001: 530-535

PEG PDS DDI

9/11

10 of 40

Boolean Constraint Propagation (BCP) Essentials

BCP consumes 80-90% of SAT run-time

What?

Identify and propagate in unit clauses (performance)

Identify and report any conflicts (correctness)

How?

Every literal l holds a Watch List -- WL(l) with all the clauses where l is watched
When literal l is falsified, visit all the clauses in WL(¬l)

c₂

c₁

c₃

c₂

c₁

c₃

c₂

c₁

c₃

Falsified literal:

Satisfied literal:

Unassigned literal:

PEG PDS DDI

10/11

11 of 40

Efficient Data Structure for BCP

GRASP watched all the literals
It is sufficient to watch two non-falsified literals: SATO’s Head/Tail!

Watching: visiting during BCP

Hantao Zhang: SATO: An Efficient Propositional Prover. CADE 1997: 272-275

Chaff’s 2WL: watching the first two literals – no need to visit during backtracking!

as long as: decision-level(falsified watch) ≥ decision-level(falsified non-watch)

Caching one literal inside the watches & inlining binary clauses

Sörensson, N., Eén, N.: MiniSAT 2.1 and MiniSAT++ 1.0 - SAT race Editions. SAT, Competitive Event Booklet (2008) (caching one literal)� Geoffrey Chu, Aaron Harwood, Peter J. Stuckey: Cache Conscious Data Structures for Boolean Satisfiability Solvers. J. Satisf. Boolean Model. Comput. 6(1-3): 99-120 (2009) (caching one literal & inlining binary clauses)

2/18/2024

c₄

c₅

c₇

c₂

c₁

c₃

c₆

Falsified literal:

Satisfied literal:

Unassigned literal:

Unknown literal:

Non-falsified literal:

Non-satisfied literal:

c₄

c₅

c₇

c₃

c₂

c₆

c₁

PEG PDS DDI

11/11

12 of 40

Conflict Analysis Loop in Chaff

Right-hand side: the conflict

Left-hand side: the reason, including the rightmost Unique Implication Point (UIP) of the last level

f@5(C₅)

Decision Level 4

f@1(C₇)

c@3

¬f@3(C₆)

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ f

a@1

b@2

c@3

d@4

e@5

g@5

¬g@5

f@5

e@5

c@3

b@2

1UIP

C₆=¬f ∨ ¬c ∨ ¬b

a@1

b@2

C₃

C₄

C₅

C₄

g@3

¬g@3

a@1

¬f@3

C₁

C₂

1UIP

C₇=f ∨ ¬a

a@1

c@3

b@2

Learn a falsified asserting clause C=[c₁^@δ, c₂^@β<δ, c₃^@≤β, … , c_|C|^{@≤ β}]

1UIP clause in Chaff

Backtrack to level β: called Non-Chronological Backtracking (NCB) in Chaff 🡪 C becomes unit
Flip & imply c₁in its parent C and run BCP

NCB to 3

NCB to 1

Decision Level 1

Decision Level 2

Decision Level 3

Decision Level 5

Decision variable/literal

Implication graph

g@5(C₃)

g@3(C₁)

PEG PDS DDI

12/11

13 of 40

Conflict Analysis Loop in GRASP

b@2

a@1

g@3

a@1

b@2

c@3

d@4

e@5

f@5(C₅)

g@5

¬g@5

f@5

e@5

c@3

1UIP

C₆=¬f ∨ ¬c ∨ ¬b

C₃

C₄

C₅

C₄

2UIP 🡪 1UIP

C₇=¬e ∨ f

¬f@3(C₆)

a@1

b@2

c@3

d@4

f@1(C₈)

a@1

¬f@3

C₁

C₂

1UIP

c@3

b@2

2UIP🡪1UIP

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ f

b@2

C₉=¬c ∨ ¬b ∨ ¬f

C₈=f∨ ¬a

Backtrack to the conflict level δ: called NCB in GRASP
Learn a falsified asserting 1UIP clause C=[c₁^@δ, c₂^@β<δ, c₃^@≤β, … , c_|C|^{@≤ β}]
Learn a clause per every other UIP of the last level
Backtrack to level δ-1: called Chronological Backtracking (CB) in later literature!
Flip & imply c₁in its parent C and run BCP

CB to 4

¬g@3

Backtrack to conflict level 3

CB to 2

In GRASP, f is a special kind of a “flipped” decision variable at level 5, but GRASP learns as if ¬f were implied at level 3

g@5(C₃)

g@3(C₁)

¬g@1(C₄)

¬c@1(C₃)

PEG PDS DDI

13/11

14 of 40

Up-to-date Conflict Analysis Loop Algorithm �Covers GRASP & Chaff & Modern Solvers

Backtrack before conflict analysis: backtrack to the conflict level δ, if required

Required in GRASP and called Non-Chronological Backtracking (NCB) in GRASP
Not required in Chaff: current decision level ≡ conflict level

Learn an asserting clause C=[c₁^@δ, c₂^@β<δ, c₃@^@≤β, …, c_i@^@≤β, …, c_|C|^@≤β]

1UIP clause in both GRASP & Chaff

Optionally, learn other clauses

GRASP: a clause for every other UIP of the conflict decision level

Backtrack: backtrack to a level in [β, β+1, …, δ-1] -- makes the asserting clause unit

GRASP -- always δ-1: Chronological Backtracking (CB) in today’s terminology
Chaff -- always β: Non-Chronological Backtracking (NCB) in today’s terminology

Flip c₁ by implying it in C and run BCP

PEG PDS DDI

14/11

15 of 40

Conflict Analysis Loop Evolvement

Maple_LCM_Dist_ChronoBT (MapleCB): Chronological Backtracking (CB) strikes back

Alexander Nadel, Vadim Ryvchin: Chronological Backtracking. SAT 2018: 111-121

A backtracking heuristic choosing between CB and NCB

Today: Maple-based solvers, Cryptominisat, Kissat alter between CB and NCB

CB algorithm is similar to GRASP’s
Integrating CB with post-GRASP data structures for BCP (Watch Lists) turned out to be non-trivial

Because of simultaneous propagation at several levels
BCP must be adjusted to prevent correctness & performance issues
Useful BCP invariants are still violated

Cadical’19: custom (score-based) backtracking

Sibylle Möhle, Armin Biere: Backing Backtracking. SAT 2019: 250-266

Backtrack to the decision level with the highest variable score
Applied by Cadical & IntelSAT

CB & BCP integration: implemented, but not discussed

1996

GRASP

2001

Chaff

2018

Maple_LCM_Dist_ChronoBT

2019

Cadical’19

Chaff’s alg. (one 1UIP cls. & NCB) is the state-of-the-art

PEG PDS DDI

15/11

16 of 40

Integrating CB and BCP

Example of a necessary adjustment

¬c₁ and ¬c₂ are assigned @1 < max_level(C)

Can’t happen with NCB, where the assigned level is always ≥ max_level(C)

Must swap lit’s & update WL’s to watch two highest falsified lit’s
Essential for correctness – in order not to miss conflicts after backtracking!

Useful invariants are still violated even with the adjustments:

lowest implication: no assigned literal can be implied at a lower level
lowest conflict: every conflict, BCP returns a clause �falsified at the lowest possible level

Intel® SAT Solver (IntelSAT): lowest implication & lowest conflict ensured!

Alexander Nadel: Introducing Intel® SAT Solver. SAT 2022.

Alexander Nadel, “Introducing Intel® SAT Solver” [video], MIAO Seminars. February 2023.

@30

c₂

@20

c₁

@30

@20

@30

Falsified literal:

Unassigned literal:

@10

@20

@10

Satisfied literal:

@30

@20

PEG PDS DDI

16/11

17 of 40

Intel® SAT Solver (IntelSAT)

An open-source CDCL solver written from scratch in C++20

Alexander Nadel: Introducing Intel® SAT Solver. SAT 2022.
Alexander Nadel, “Introducing Intel® SAT Solver” [video], MIAO Seminars. February 2023.

License: MIT (free)

Public repository: https://github.com/alexander-nadel/intel_sat_solver

Tuned towards incremental applications with mostly SAT queries

Paper: anytime unweighted MaxSAT
@Intel: optimization problems – placement, scheduling, etc.

2/18/2024

PEG PDS DDI

17/11

18 of 40

Optimization in SAT

OptSAT(F, ψ): given a propositional formula F in CNF and a Pseudo-Boolean objective function ψ, return a model to F which minimizes ψ

A Pseudo-Boolean (PB) function: a mapping from every full assignment to a real number

2/18/2024

Example: F = (a + b) (a + ¬c) (¬a + c)

F has 3 models:

M₁={a=0, b=1, c=0}
M₂={a=1, b=0, c=1}
M₃={a=1, b=1, c=1}

a	b	c	ψ
0	0	0	2.3
0	0	1	3.5
0	1	0	8
0	1	1	100.1
1	0	0	96.3
1	0	1	75
1	1	0	1.35
1	1	1	20.4

PEG PDS DDI

18/11

19 of 40

Optimization in SAT

OptSAT(F, ψ): given a propositional formula F in CNF and a Pseudo-Boolean objective function ψ, return a model to F which minimizes ψ

A Pseudo-Boolean (PB) function: a mapping from every full assignment to a real number

2/18/2024

Example: F = (a + b) (a + ¬c) (¬a + c)

F has 3 models:

M₁={a=0, b=1, c=0}
M₂={a=1, b=0, c=1}
M₃={a=1, b=1, c=1}

a	b	c	ψ
0	0	0	2.3
0	0	1	3.5
0	1	0	8
0	1	1	100.1
1	0	0	96.3
1	0	1	75
1	1	0	1.35
1	1	1	20.4

Best model

PEG PDS DDI

19/11

20 of 40

Solving OptSAT(F, ψ) Instances in Real-life

Is ψ is a linear PB function: ψ = w_n-1*t_n-1 + … + w₁*t₁ + … + w₀*t₀?

t_i’s are Boolean variables
w_i’s are strictly positive integer coefficients
Example: ψ = 2*t₂ + 5*t₁ + 7*t₀

2/18/2024

Yes

MaxSAT: a rich well-established field!

Scarce research

Our contribution

Polosat algorithm: simulate local search with SAT (Nadel, FMCAD’20)

Very efficient and simple to implement
In focus today

High-level local search with SAT/Polosat as an oracle �(Cohen&Nadel&Ryvchin, TACAS’22)

PEG PDS DDI

20/11

21 of 40

Polosat: Black-Box Optimization in SAT

Polosat: minimize a black-function ψ(V), given F(V) -- incomplete

How to use Polosat:

Similarly to SAT, create the CNF formula by adding clauses
Call the SAT solver (possibly under assumptions) with ψ as a callback function

The solver will query ψ, when all the variables are assigned
The solver expects to get back a number

No need to bit-blast ψ into clauses: calculate ψ in the callback instead!

In practice:

ψ depends only on observables B= {b_n-1, … , b₀} ⊆ V, and
ψ is strictly monotone in B: b_i∈B flipped from 1 to 0 🡪 ψ is decreased

Example: MaxSAT, where ψ = w_n-1*b_n-1 + … + w₁*b₁ + … + w₀*b₀

these restrictions can be lifted

PEG PDS DDI

21/11

22 of 40

Polosat Algorithm: Simulate Local Search with SAT

Polosat (CNF F(V), black-box objective function ψ(V), observables B ⊆ V)

M := SAT(F)
External loop: run the following internal loop until M is not improved anymore

Internal loop: go over all the bad observables (bad: never assigned 0 in any model)

Try to flip the current bad observable b:

M’ := SAT(F, {¬b}) (¬b is an assumption which holds during only the current query)

If (satisfiable and ψ(M’) < ψ(M)) M := M’

Return M

No model can be rediscovered by construction

Making Polosat work in practice:

Apply polarity-fixing in all the SAT invocations to simulate local search

TORC heuristic: fix the observables to 0 and the rest to the best model so far M

Use a conflict threshold N (N=1000): limit every SAT call (except for the 1^st one) by N conflicts
Decision heuristic modification: initial boost to the scores of the observables can also be useful

2/18/2024

PEG PDS DDI

22/11

23 of 40

Polosat Cont.

Polosat is an incomplete algorithm

Polosat can be integrated into a high-level complete algorithm by �replacing SAT queries to Polosat queries

Next -- applying Polosat to boost:

Industrial Cell Placement
Anytime MaxSAT Solving

PEG PDS DDI

23/11

24 of 40

Cell Placement without Optimization: Input

2/18/2024

The grid where to place the cells

The cells to be placed

c₁

c₂

c₃

c₄

c₅

Cell Placement w/o Opt.: Output

The cells are placed
Already NP-complete!

PEG PDS DDI

24/11

25 of 40

Cell Placement Input

2/18/2024

n₁



n₂

n₁
n₂	n₃

n₁

The grid where to place the cells

The cells to be placed

c₁

c₂

c₃

c₄

c₅

N nets: n₁={c₁,c₃,c₅}; n₂={c₂,c₃}; n_N=3={c₃,c₄}

n₃

Industrial practice: additional constraints!

PEG PDS DDI

25/11

26 of 40

Cell Placement Input

2/18/2024

n₁



n₂

n₁
n₂	n₃

n₁

The grid where to place the cells

The cells to be placed

c₁

c₂

c₃

c₄

c₅

N nets: n₁={c₁,c₃,c₅}; n₂={c₂,c₃}; n_N=3={c₃,c₄}

n₃

n₁

n₁

n₁
n₂	n₃



n₂

n₃

Cell Placement with Opt. Output

Net size |n_i| of n_i: the perimeter of n_i’s bounding box B_i
Minimize placement size: the sum of all the net sizes

B₁

B₂

B₃

Industrial practice: additional constraints!

PEG PDS DDI

26/11

27 of 40

Cell Placement 🡪 BV/SAT : Constraints

2/18/2024

To find a solution: ensure there is no overlap between each pair of cells

and all the cells are placed inside the grid (skipped here)

PEG PDS DDI

27/11

28 of 40

Solving Placement with Optimization Modulo Bitvectors (OBV)

2/18/2024

A BV variable for the net size for each net:

The OBV target T = n₁+n₂+…+n_N

OBV goal: minimize T

PEG PDS DDI

28/11

29 of 40

Solving OBV(F,T) with SAT-based Linear Search

2/18/2024

Complete anytime algorithm

anytime algorithm: finds better and better solutions, the longer it keeps running

Outperforms other OBV algorithms (binary-search-based)
Still, gets stuck far from the optimum on industrial placement instances

bit-vector addition (in the target) is too heavy

PEG PDS DDI

29/11

30 of 40

Polosat for Placement

Integration: Polosat invocations replace SAT invocations inside linear search

simply returns the value of T under the current model

Observables B = all the bits of {n₁, n₂, …, n_N}; ψ is monotone in B

A BV variable for the net size for each net:

The OBV target T = n₁+n₂+…+n_N

PEG PDS DDI

30/11

31 of 40

Experimental Results: Industrial Cell Placement Benchmarks (our TACAS’21 paper)

1200 proprietary industrial designs of various sizes and complexities.
Algorithms:

{OBV with Binary search, OBV with Linear search, LSSO} x {SAT, Polosat}

LSSO: Local Search with SAT/Polosat as an Oracle (our TACAS’21 paper)

Maximal timeout: 600 sec.

Intermediate timeouts: 50, 100, 150, 200, 250, 300, 350, 400, 450, 500

Score = best Σ(net-sizes) / my Σ(net-sizes)

normalized to [0, 1] for every timeout
1: the absolutely best result within the timeout (the virtual best)
the closer to 1 the better

2/18/2024

PEG PDS DDI

31/11

32 of 40

Linear vs Binary & Polosat impact

Linear search with SAT (ls_no_polosat) outperforms binary search with SAT (bs_no_polosat)
Linear search with Polosat (ls) outperforms linear search with SAT (ls_no_polosat)

Linear search with Polosat (ls): the best published result

LSSO with SAT/Polosat as an Oracle

Best LSSO with SAT (many_env_spec_hill_clmb_no_polosat) is only slightly outperformed by linear search with Polosat (the previous best)
Best LSSO with Polosat outperforms the linear search with Polosat (the previous best)
Out Polosat-based tool has been successfully productized at Intel!
Each of the LSSO algorithms contributes to the virtual best

see the paper

2/18/2024

PEG PDS DDI

32/11

33 of 40

Polosat for MaxSAT: our FMCAD’20 Paper

Integrated into the anytime MaxSAT solver TT-Open-WBO-Inc

Winner of MSE’19 in both the weighted, incomplete categories

Integration: replaced SAT invocations by Polosat invocations

Used adaptive strategy to stop Polosat forever, when it gets too slow

Gets too slow: generates less than 1 new model per second

2/18/2024

PEG PDS DDI

33/11

34 of 40

Polosat for MaxSAT: Results

2/18/2024

Benchmarks: 297 MSE’19 benchmarks in weighted, incomplete categories

Timeout: 1800 sec.

Score: [0, 1]: 1 is the best

Solvers:

Polosat

NoComb: A Polosat variation

NoCC: A Polosat variation

TT-Open-WBO-Inc: MSE’19 winner

NoAdapt: No adaptive strategy

Loandra: MSE’19 runner-up

Main Observation:

Polosat substantially improves TT-Open-WBO-Inc!

PEG PDS DDI

34/11

35 of 40

Polosat: Status

Enabler for solving industrial optimization problems at Intel

Default in state-of-the-art anytime MaxSAT solvers

Used by the top 3 solvers in all the 4 anytime categories @ MaxSAT Evaluation 2023

NuWLS-2023 (the winner): preprocessing with local search + TT-Open-WBO-Inc
Categories: {weighted,unweighted} X {60 sec. to, 300 sec. to}

Recently shown to boost Pseudo-Boolean (PB) Optimization

PB Optimization: optimizing an objective function under PB constraints

Markus Iser , Jeremias Berg, Matti Järvisalo:�Oracle-Based Local Search for Pseudo-Boolean Optimization. ECAI 2023: 1124-1131

PEG PDS DDI

35/11

36 of 40

Solving Complex (Non-Linear) Optimization Problems is an Opportunity for the SAT Community!

Currently, SAT-based verification comprises SAT’s heaviest industrial usage

But what about industrial optimization problems?

Alternative: mixed-integer nonlinear programming (MINP)

Might not work in the presence of complex Boolean constraints, where SAT-based solutions are expected to be a better fit (similarly to MaxSAT vs. ILP in linear case)
Optimizing black-box functions in MINP is not explored

A SAT-based solution is already productized @ Intel for placement and scheduling!

PEG PDS DDI

36/11

37 of 40

Backup

PEG PDS DDI

37/11

38 of 40

SAT Application Examples

2/18/2024

SAT@

PEG PDS DDI

38/11

39 of 40

IntelSAT Concepts

Incremental Lazy Backtracking (ILB)

In-between incremental queries, backtrack only when necessary and to the highest possible level

Other solvers backtrack all the way to level 0

Reimplication: new core SAT algorithm

Reimplies assigned literals at lower levels without backtracking
Enables ILB
Independently of ILB, restores the two core BCP invariants, broken by Chronological Backtracking (CB)

Trail implemented as doubly-linked list (rather than stack) to facilitate CB & reimplication

No pointers, efficient array-based implementation

New heuristics (query-driven tuning, subsumption-based flipped clause filtering, incr. score reboot)

No heavy algorithms, such as, inprocessing and vivification

2/18/2024

PEG PDS DDI

39/11

40 of 40

Solving Complex Optimization Problems with SAT: �Ideas for Future Research

Classic (non-SAT-based) local search

Dedicated algorithms for sub-classes of optimization functions

Going beyond SAT and Pseudo-Boolean constraints

Finding more applications

PEG PDS DDI

40/11