Slide1: Complexity Analysis of a Massively Parallel Boolean Satisfiability Implication Circuit
Ph.D. Defense
By Mark J. Boyd
Chair Tracy Larrabee
Reader Andrea Di Blas
Reader Richard Hughey
Significant and Novel Research: Significant and Novel Research Analyzed O(mn) parallelism for SAT
Showed unroutability of FPGA approach
Demonstrated floorplanned solution
Overview: Overview Synopsis of the research
Boolean satisfiability (SAT)
Previous FPGA parallel approaches
Zhong (Princeton) instance-specific
Unroutable with claimed resources
My floorplanned approach
ELVIS single chip
PRISCILA multi-chip
Conclusion
Overview - Research: Overview - Research Research interests
Boolean satisfiability
Fundamental open problem with currently exponential runtime
FPGAs
Parallel applications
Rapid prototyping
Dynamic rerouting
I implemented a regular floorplan methodology
ELVIS
Single chip design
Easily and quickly loaded
PRISCILA
Multi-chip design explicitly showing external routing scalability
Overview - Motivations: Overview - Motivations FPGA approach has long compile times
Field Programmable Custom Computing Machines Conference
We showed routing problem unscalable
We presented a regular generalized layout
Need to evaluate wide clauses in parallel
GRASP and zchaff software
Clause addition helps scalable speedup – GOOD!
Wide clauses take time to evaluate – BAD!
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
k=3, maximum clause width
n=4, number of variables
m=5, number of clauses
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
k=3, maximum clause width
n=4, number of variables
m=5, number of clauses
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
k=3, maximum clause width
n=4, number of variables (A,B,C,D)
m=5, number of clauses
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
k=3, maximum clause width
n=4, number of variables
m=5, number of clauses
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
k=3, maximum clause width
n=4, number of variables
m=5, number of clauses
L=13, number of literals
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+B+C)(F+B)(B+C)(A+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+B+C)(F+B)(B+C)(F+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+B+C)(F+B)(B+C)(F+B+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+C)(F+B)(B+C)(F+B+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+C)(F+T)(B+C)(F+B+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+C)(F+T)(T+C)(F+B+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+C)(F+T)(T+C)(F+F+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+F)(F+T)(T+C)(F+F+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+F)(F+T)(T+T)(F+F+C)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+F)(F+T)(T+T)(F+F+T)(F+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T T
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T T T
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T T T T
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T T T T T
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
T T T T T = TRUE
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
But wouldn’t it be nice if all of these operations happened simultaneously?
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
But wouldn’t it be nice if all of these operations happened simultaneously?
T T T T T = TRUE
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
We’ll get there soon…
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[B=1] is a partial truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(A+B+C)(A+F)(B+C)(A+B+C)(A+C+D)
[B=1] is a partial truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(A+B+C)(A+F)(B+C)(A+B+C)(A+C+D)
[B=1] implies [A=0] because A must now be assigned 0 to make the clause true
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(A+B+C)(T+F)(B+C)(A+B+C)(A+C+D)
[B=1] implies [A=0]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(F+B+C)(T+F)(F+C)(A+B+C)(A+C+D)
[B=1] implies [A=0]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(F+B+C)(T+F)(F+C)(A+B+C)(A+C+D)
[B=1] implies [A=0,C=0]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
What is a transitive implication?
(F+B+C)(T+F)(F+T)(A+B+C)(A+C+D)
[B=1] implies [A=0,C=0], called transitive implications
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables…
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[A=1,C=1] is a partial truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables…
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)
[A=1,C=1] is a partial truth assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables…
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)
[A=1,C=1] implies [B=0,B=1]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)
[A=1,C=1] implies [B=0,B=1] ?
But that’s a contradiction, right?
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables…
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)
[A=1,C=1] implies [B=0,B=1]
Because it results in a contradiction, [A=1,C=1] cannot be a part of any satisfying assignment
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s restart and try more variables…
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)(A+C)
[A=1,C=1] implies [B=0,B=1]
Because [A=1,C=1] cannot be a part of any satisfying assignment we can add a clause forbidding it. DeMorgan (A*C) = (A+C)
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
But wouldn’t it be nice if all of these operations happened simultaneously?
(A+B+C)(F+B)(B+F)(F+B+F)(A+C+D)(A+C)
[A=1,C=1] implies [B=0,B=1]
We’ll get there…
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s try a really big problem
(A+B+C+D+G)(A+B+C+E+H)(A+B+D+E+I)
(A+C+D+E+J)(B+C+D+E+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0] implies
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s try a really big problem
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0] implies
[G=1,H=1,I=1,J=1,K=1]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s try a really big problem
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0] implies
[G=1,H=1,I=1,J=1,K=1]
Boolean satisfiability (SAT)
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s try a really big problem
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(F+F+F+F+F)
[A=0,B=0,C=0,D=0,E=0] implies
[G=1,H=1,I=1,J=1,K=1], which creates a falsified clause
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
Let’s try a really big problem
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(F+F+F+F+F)
[A=0,B=0,C=0,D=0,E=0] cannot be a part of any satisfying truth assignment, add
(A+B+C+D+E)
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
25 operations in parallel?
(A+B+C+D+G)(A+B+C+E+H)(A+B+D+E+I)
(A+C+D+E+J)(B+C+D+E+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0]
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
25 operations in parallel?
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0] implies
[G=1,H=1,I=1,J=1,K=1]
Wouldn’t THAT be something…
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
25 operations in parallel?
(F+F+F+F+G)(F+F+F+F+H)(F+F+F+F+I)
(F+F+F+F+J)(F+F+F+F+K)(G+H+I+J+K)
[A=0,B=0,C=0,D=0,E=0] implies
[G=1,H=1,I=1,J=1,K=1]
For k=O(n)=O(m), O(mn) parallelism
Boolean satisfiability (SAT): Boolean satisfiability (SAT) For any m, randomly pick m/2 variables for each clause
Append a new unique variable to each clause
Add one clause with the negations of all the appended variables
A partial assignment of true to the first m variables implies all of the appended variables true
Contradicts the final clause
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
25 operations in parallel?
(A+B+C+D+G)(A+B+C+E+H)(A+B+D+E+I)
(A+C+D+E+J)(B+C+D+E+K)(G+H+I+J+K)
A problem which supports O(mn) speedup by parallel literal evaluation
Boolean satisfiability (SAT): Boolean satisfiability (SAT) For SOME k-SAT formulas, evaluating all literals and clause implications in a single operation provides O(mn) parallelism over serial literal operations.
Purpose of parallelism for speedup of SAT: Purpose of parallelism for speedup of SAT Calculating transitive implications, Boolean Constraint Propagation (BCP)
Commonly 90 to 99% of the total runtime
Excellent heuristics of GRASP or zchaff software speed up solution
Addition of wide 'conflict' clauses avoids repetitive search
Avoids evaluating unneeded clauses
BUT…software heuristics still slow for some densely connected unsatisfiable problems
Hole, hgen benchmarks of about 260 variables
Parallel FPGA approaches: Parallel FPGA approaches
Zhong (Princeton) instance-specific mapping of a formula to an FPGA
State machine generates partial assignments to send to IMP circuit
IMP circuit calculates implications and sends back results
Parallel FPGA approaches: Parallel FPGA approaches
Zhong (Princeton) instance-specific mapping of a formula to an FPGA
Each clause is made into a gate for each variable
But this is a bipartite graph 2-Level Planarization problem: NP-hard for areaandlt;O(n )
2
What is an FPGA?: What is an FPGA?
An array of logic and memory
Logic cells (4x4 memory)
A mesh of routing
Crossbar switchboxes (4x4) supporting flexible interconnect
Parallel FPGA – P&R: Parallel FPGA – Pandamp;R
Zhong (Princeton) instance-specific mapping requires Pandamp;R
Each clause is made into a gate for each variable
But this is a bipartite graph 2-Level Planarization problem: NP-hard for areaandlt;O(n )
2
Parallel FPGA – P&R: Parallel FPGA – Pandamp;R 1
2
3
4
5
6
Zhong gate blowup for big k: Zhong gate blowup for big k
Zhong (Princeton) instance-specific mapping of a formula to an FPGA
Wide clause made into gates = BIG
Example:
Clause from hole10
Even gates grow as O(k m) (1+2+3+4+5+6+7+8+9+10) 2
General Floorplan of ELVIS: General Floorplan of ELVIS
Shift Register Bus Mask: Shift Register Bus Mask Eliminate routing problem by
Routing all variables to all clauses using a bus
Masking unused variable signals using a shift register
Shift Register Bus Mask: Shift Register Bus Mask Only allows the lines through that are selected by the shift register 0 0 1 1 1 0 0 1 1 0 0 0
Oneact “one active” encoder: Oneact 'one active' encoder A multi-bit unary input, two-bit result
An adder that overflows at 2
Shift Register Bus Mask: Shift Register Bus Mask
Example of CEC: Example of CEC
Example of CEC, [A=1, C=1]: Example of CEC, [A=1, C=1] 1 1 1 1 1 0 0 0 0 0 0 0
Example of VEC, [A=1, C=1]: Example of VEC, [A=1, C=1] 1 1 1 0 0 1 0 0
Example of VEC, [A=1, C=1]: Example of VEC, [A=1, C=1] 1 1 1 0 0 1 0 0 1 0 0 1
The other two variables…: The other two variables… 1
Floorplan of CECs and VECs: Floorplan of CECs and VECs VECs CECs
Partition of CECs and VECs: Partition of CECs and VECs VECs CECs
Board Layout of PRISCILA: Board Layout of PRISCILA
Overview of PRISCILA: Overview of PRISCILA 14 FPGA boards
Regular wiring with 40 wire ribbon cables
12 boards for a 3x4 rectangular array
1 board is the FSM
1 board to collect data on performance
3.1 MHz theoretical maximum
1.6 MHz tested
Cycle Speedup of PRISCILA: Cycle Speedup of PRISCILA Dubois Pretolani
Analysis : Analysis Cycles for A-SAT are really complex operations (load, load, decrement,store), so not comparable
Assumed memory latency increases with size of problem. Not necessarily true for cached, pipelined serial processor
Used a big (32 var, 48 clause) PRISCILLA for all problems. Latency not scaled.
The Hughey Amendment : The Hughey Amendment Cycles for A-SAT are really complex operations (load, load, decrement,store), so not comparable
Doesn’t matter, just want scalable speedup
Assumed memory latency increases with size of problem. Not necessarily true for cached, pipelined serial processor
Assume perfect pipe/cache, constant access times
Used a big (32 var, 48 clause) PRISCILLA for all problems. Latency not scaled.
Penalize larger problems by a factor of m (delay)
Speedup of PRISCILA: Speedup of PRISCILA
Rebuttal to Hughey Amendment : Rebuttal to Hughey Amendment Scalable speedup (between log and linear)
VS a serial processor of O(1) memory latency!
Because serial processor is O(mn) operations
Results aren’t a proof in themselves (too small) but are consistent with previous work
How can ELVIS/PRISCILA improve… : How can ELVIS/PRISCILA improve… Two major improvements
Use the carry logic in FPGAs for wide functions
Cycle speeds improved by 100x (250 MHz)
Resource usage much more efficient
Design a parallel FSM to drive the implication logic faster
Transitive implications only 90-99% of the total time
Speedups over 10-100 not generally possible except for hardest benchmarks
What can ELVIS/PRISCILLA do…: What can ELVIS/PRISCILLA do… Coprocessor for industrial problems
zchaff extraction of small cores within 2-20% of size of the minimal unsatisfiable core.
PRISCILLA detects unsatisfiable formulas 10-100 times faster (limited by state machine)
Place and route, logic minimization, verification and testing of circuits and software, airline scheduling
RECAP and Acknowledgments: RECAP and Acknowledgments
Parallel calculation of SAT
transitive implications
O(mn) over software
Instance-specific approaches unscalable
Negative result
Scalable floorplanned approach (ELVIS)
Useful for small unsatisfiable cores
Any clause width
Multi-chip (PRISCILLA)
More speedup from larger problems Acknowledgements: Kevin Klenk for help with initial state machine design. Doanna Weissgerber for help with the software loading interface. NSF funding under CCR-9971172. Xilinx for devices
and ISE software.
Slide87:
Slide88:
“P” Parallel Pipelines: 'P' Parallel Pipelines
Pipelined approach: Pipelined approach Zhong time-sliced variables through a pipeline
EXTRAS: EXTRAS
The Experiment: Results: The Experiment: Results Average times in seconds to complete all tasks for each of the 21 alignments
Experimental group 1.5 times faster
Protein Structure: Protein Structure Hierarchical Structure
Goal understand function of protein from primary structure
Sequence of protein relatively easy to obtain
Floorplan of the Approach: Floorplan of the Approach
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B)(~A+~B+~C)(~B+C)(~A+B+~D)
(~C+D)(B+C+D)(A+~C+~D)(~B+D)
k=3, maximum clause width
n=4, number of variables
m=8, number of clauses
Boolean satisfiability (SAT): Boolean satisfiability (SAT)
A k-SAT formula is a Boolean expression in conjunctive normal form (CNF)
(A+B+C)(A+B)(B+C)(A+B+C)(A+C+D)
[A=1, B=0, C=0, D=1] is an easily verified satisfying truth assignment
T T T T T = TRUE
(T+F+F)(F+T)(T+T)(F+F+T)(F+F+T)
Protein Structure: Protein Structure
Floorplan of the Approach: Floorplan of the Approach
A Critically Unsatisfiable Formula: A Critically Unsatisfiable Formula
Parallel FPGA approaches: Parallel FPGA approaches
Floorplan of the Approach: Floorplan of the Approach
Layers ofVisPad: Layers of VisPad Independent
of
RDAG-128H Dependent on
RDAG-128H
knowledge