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