1 of 41

CDCL SAT Solving and �Applications to Optimization Problems

Alexander Nadel, Intel & Technion, Israel

April 17, 2023

Satisfiability: Theory, Practice, and Beyond Workshop

Simons Institute, UC Berkeley, Berkeley, CA, USA

1

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 41

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 41

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?!

3

4/17/2023

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

clause #1

clause #2

Literals

PEG PDS DDI

3/11

4 of 41

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)

4

4/17/2023

PEG PDS DDI

4/11

5 of 41

From Enumeration to DPLL

5

4/17/2023

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

0

1

0

Carry out backtrack search.

Stop when a model is found

0

The unassigned literal c₁must be implied

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

clause #1

clause #2

Literals

a

b

c

0

1

0

1

a

b

c

0

1

0

1

a

b

c

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:

1

a

b

c

0

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 41

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

6

4/17/2023

a

b

c

0

1

0

1

PEG PDS DDI

6/11

7 of 41

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

7

4/17/2023

PEG PDS DDI

7/11

8 of 41

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 41

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 41

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 41

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)

4/17/2023

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 41

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 41

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

C₇=¬e ∨ ¬c ∨ ¬b

¬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

C₁= ¬a ∨ f ∨ g

C₂= ¬a ∨ f ∨ ¬g

C₃= ¬c ∨ ¬f ∨ g

C₄= ¬b ∨ ¬f ∨ ¬g

C₅= ¬e ∨ f

b@2

C₉=¬c ∨ ¬b ∨ ¬a

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₁)

PEG PDS DDI

13/11

14 of 41

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 41

Conflict Analysis Loop Evolvement

Maple_LCM_Dist_ChronoBT (MapleCB): the return of Chronological Backtracking (CB)

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 highly 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 41

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

@1

@20

@1

@20

@1

@30

Falsified literal:

Unassigned literal:

@10

@20

@10

Satisfied literal:

@1

@30

@1

@30

@1

@20

@1

@20

PEG PDS DDI

16/11

17 of 41

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.

17

4/17/2023

PEG PDS DDI

17/11

18 of 41

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

18

4/17/2023

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 41

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

19

4/17/2023

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 41

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₀

20

4/17/2023

Yes

No

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 41

Polosat: Black-Box Optimization in SAT

Polosat: minimize a black-function ψ(V), given the SAT formula F(V)

How to use Polosat:

Similarly to SAT, create the CNF formula by adding clauses
Call the SAT solver (possibly under assumptions), but also provide ψ 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 41

Polosat Algorithm: Simulate Local Search with SAT

Polosat (F, ψ, T)

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}) (¬t is an assumption)

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
Initial boost to the VSIDS scores of the observables can also be useful

22

4/17/2023

PEG PDS DDI

22/11

23 of 41

Polosat: Incomplete vs. Complete

Polosat is an incomplete algorithm

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

PEG PDS DDI

23/11

24 of 41

Cell Placement without Optimization: Input

24

4/17/2023

0

8

The grid where to place the cells

The cells to be placed

c₁

c₂

c₃

c₄

c₅

0

8

Cell Placement w/o Opt.: Output

The cells are placed
Already NP-complete!

PEG PDS DDI

24/11

25 of 41

Cell Placement Input

25

4/17/2023

n₁



n₂

n₁
n₂	n₃

n₁

0

8

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₃

PEG PDS DDI

25/11

26 of 41

Cell Placement Input

26

4/17/2023

n₁



n₂

n₁
n₂	n₃

n₁

0

8

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₃

0

8

n₁

n₁

n₁
n₂	n₃



n₂

n₃

Net size |n_i| of n_i: the perimeter of n_i’s bounding box B_i

B₁

B₂

B₃

PEG PDS DDI

26/11

27 of 41

Cell Placement Input

27

4/17/2023

n₁



n₂

n₁
n₂	n₃

n₁

0

8

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₃

0

8

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

27/11

28 of 41

Cell Placement 🡪 BV/SAT : Constraints

28

4/17/2023

i

j

i

j

i

j

i

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

28/11

29 of 41

Solving Placement with Optimization Modulo Bitvectors (OBV)

29

4/17/2023

A BV variable for the net size for each net:

i

1

2

3

4

5

1

2

3

4

5

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

OBV goal: minimize T

PEG PDS DDI

29/11

30 of 41

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

30

4/17/2023

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

30/11

31 of 41

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:

1

2

3

4

5

1

2

3

4

5

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

PEG PDS DDI

31/11

32 of 41

Experimental Results: Industrial Cell Placement Benchmarks (our TACAS’22 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’22 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

32

4/17/2023

PEG PDS DDI

32/11

33 of 41

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 tool has been successfully productized at Intel!
Each of the LSSO algorithms contributes to the virtual best

see the paper

33

4/17/2023

PEG PDS DDI

33/11

34 of 41

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

34

4/17/2023

PEG PDS DDI

34/11

35 of 41

Polosat for MaxSAT: Results

35

4/17/2023

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

35/11

36 of 41

Polosat: Status

Polosat is an enabler for solving industrial optimization problems at Intel

Polosat was used by the winner of the MaxSAT Evaluation 2022 in all the incomplete categories

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

PEG PDS DDI

36/11

37 of 41

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

37/11

38 of 41

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 constraints (Pseudo-Boolean)

Finding more applications

PEG PDS DDI

38/11

39 of 41

Backup

PEG PDS DDI

39/11

40 of 41

SAT Application Examples

40

4/17/2023

SAT@

PEG PDS DDI

40/11

41 of 41

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

41

4/17/2023

PEG PDS DDI

41/11