Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: A B C D E G I M P R S V X

A
Algebraic reasoning	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
automated reasoning	Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
B
Binary Decision Diagrams	TBUDDY: A Proof-Generating BDD Package Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
Block Ciphers	Towards an Efficient CNF Encoding of Block Ciphers
Boolean Satisfiability	Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
C
CDCL Algorithm	SATViz: Real-Time Visualization of Clausal Proofs
certifying solvers	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
clausal proofs	TBUDDY: A Proof-Generating BDD Package Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
Clause exchange	DPS: A Framework for Deterministic Parallel SAT Solvers
CNF Encoding	Towards an Efficient CNF Encoding of Block Ciphers Calculating Sufficient Reasons for Random Forest Classifiers
cutting planes	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
D
DNF	Dinosat: A SAT Solver with Native DNF Support
dominance	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
dual variables	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
E
encoding	Towards the shortest DRAT proof of the Pigeonhole Principle
G
Gauss-Jordan Elimination	Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
Gaussian elimination	TBUDDY: A Proof-Generating BDD Package
I
Incremental SAT Solving	Calculating Sufficient Reasons for Random Forest Classifiers
M
Multi-Threaded Solving	Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
multiplier verification	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
P
Parallel Reasoning	Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Pigeonhole principle	Towards the shortest DRAT proof of the Pigeonhole Principle
polynomial calculus	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Portfolio parallel SAT solver	DPS: A Framework for Deterministic Parallel SAT Solvers
Prime Implicants	Calculating Sufficient Reasons for Random Forest Classifiers
Product Configuration	Dinosat: A SAT Solver with Native DNF Support
proof logging	Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
proof of unsatisfiability	Towards the shortest DRAT proof of the Pigeonhole Principle
pseudo-Boolean reasoning	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
Python Scikit-learn	Calculating Sufficient Reasons for Random Forest Classifiers
R
Random Forest Classifier	Calculating Sufficient Reasons for Random Forest Classifiers
Reproducible parallel SAT solving	DPS: A Framework for Deterministic Parallel SAT Solvers
S
SAT solver	Dinosat: A SAT Solver with Native DNF Support
SAT solving	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses SATViz: Real-Time Visualization of Clausal Proofs
Straight-line programs	Towards an Efficient CNF Encoding of Block Ciphers
Sufficient Reasons	Calculating Sufficient Reasons for Random Forest Classifiers
symmetry breaking	Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
V
Visualization	SATViz: Real-Time Visualization of Clausal Proofs
X
XOR-CNF	Towards an Efficient CNF Encoding of Block Ciphers