SAT 2016: 19TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
GLOBAL TALK KEYWORD INDEX

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

Shortcuts: 2ABCDEFGHIKLMNOPQRSTV
2
2QBF
(SAT 2016)
Incremental Determinization
A
And-inverter graphs (AIGs)
(SAT 2016)
Heuristic NPN classification for large functions using AIGs and LEXSAT
approximation
(SAT 2016)
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
(STRUCTSAT 2016)
Complexity and Approximability for Parameterized MAXCSPs
auto tuning
(SAT 2016)
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Autocorrelation Length
(SAT 2016)
The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
Automated Configuration
(SAT 2016)
SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
average-case hardness
(SAT 2016)
On the Hardness of SAT with Community Structure
Axiom pinpointing
(SAT 2016)
BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
axioms
(SAT 2016)
Q-Resolution with Generalized Axioms
B
B2B
(POS-16)
A Study on Implied Constraints in a MaxSAT Approach to B2B Problems
Backdoors
(SAT 2016)
Strong Backdoors for Default Logic
benchmark analysis
(POS-16)
Better Evaluations by Analyzing Benchmark Structure
beta-acyclic formulas
(STRUCTSAT 2016)
Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas
binary decision diagrams
(SAT 2016)
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
bit-vectors
(SAT 2016)
Deciding Bit-Vector Formulas with mcSAT
Blackbox Fuzz Testing
(SAT 2016)
SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
branch decomposition
(SAT 2016)
A SAT Approach to Branchwidth
Branching
(SAT 2016)
Extreme Cases in SAT Problems
branching heuristic
(SAT 2016)
Learning Rate Based Branching Heuristic for SAT Solvers
C
cardinality constraints
(STRUCTSAT 2016)
CNF Encoding of Cardinality Constraints via Tree-Decomposition
CDCL
(SAT 2016)
Extreme Cases in SAT Problems
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
CDCL heuristics
(POS-16)
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
CDCL SAT Solvers
(STRUCTSAT 2016)
Experiments with CNF Structure and Hardness
cegar
(SAT 2016)
2QBF: challenges and solutions
(SAT 2016)
Non-prenex QBF Solving using Abstraction
Certificates
(SAT 2016)
Incremental Determinization
Clashing-Neighbor Relation
(POS-16)
The Clashing-Neighbor Relation for Propositional Formulas
clause learning
(SAT 2016)
Q-Resolution with Generalized Axioms
Cloud computing
(SAT 2016)
OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Cluster Analysis
(POS-16)
The Clashing-Neighbor Relation for Propositional Formulas
Combinatorial Optimization
(SAT 2016)
The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
combinatorics
(SAT 2016)
Computing Maximum Unavoidable Subgraphs using SAT Solvers
Community Structure
(SAT 2016)
On the Hardness of SAT with Community Structure
(STRUCTSAT 2016)
Experiments with CNF Structure and Hardness
complex networks
(STRUCTSAT 2016)
Pseudo-Industrial Random SAT Generators
conflict-driven clause learning
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
conflict-driven clause learning solvers
(SAT 2016)
On the Hardness of SAT with Community Structure
conflict-driven clause-learning
(SAT 2016)
Learning Rate Based Branching Heuristic for SAT Solvers
constraint satisfaction problems
(STRUCTSAT 2016)
Complexity and Approximability for Parameterized MAXCSPs
Counting
(SAT 2016)
Solution-Graphs of Boolean Formulas and Isomorphism
Cryptanalysis
(POS-16)
Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions
cube learning
(SAT 2016)
Q-Resolution with Generalized Axioms
Cube-and-conquer
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
D
decomposable negation normal form
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
Default Logic
(SAT 2016)
Strong Backdoors for Default Logic
deficiency
(STRUCTSAT 2016)
Minimal unsatisfiability and deficiency: recent developments
dependency schemes
(SAT 2016)
Dependency Schemes for DQBF
(SAT 2016)
Long Distance Q-Resolution with Dependency Schemes
(STRUCTSAT 2016)
Using Decomposition-Parameters for QBF: Mind the Prefix!
(QBF 2016)
Dependency Schemes in QBF Calculi: Semantics and Soundness
Difference Logic
(SAT 2016)
Speeding Up the Constraint-Based Method in Difference Logic
diversification
(POS-16)
Approximate History Map for Massively Parallel Environments
DPLL
(SAT 2016)
Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
DQBF
(SAT 2016)
Dependency Schemes for DQBF
(SAT 2016)
Lifting QBF Resolution Calculi to DQBF
DRAT proofs
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
E
Eigenvector Analysis
(POS-16)
The Clashing-Neighbor Relation for Propositional Formulas
Empirical Hardness
(STRUCTSAT 2016)
Experiments with CNF Structure and Hardness
Encoding
(SAT 2016)
Speeding Up the Constraint-Based Method in Difference Logic
F
finite model building
(SAT 2016)
Finding Finite Models in Multi-Sorted First Order Logic
finite model finding
(SAT 2016)
Finding Finite Models in Multi-Sorted First Order Logic
first-order theorem proving
(SAT 2016)
Predicate elimination for preprocessing in first-order theorem proving
Fitness Landscape
(SAT 2016)
The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
fixed-parameter tractability
(QBF 2016)
Dynamic Programming-based QBF Solving
full clauses
(STRUCTSAT 2016)
Minimal unsatisfiability and deficiency: recent developments
G
generalized tic-tac-toe
(QBF 2016)
QBF Encoding of Generalized Tic-Tac-Toe
generating explanations
(SAT 2016)
Deciding Bit-Vector Formulas with mcSAT
graph theory
(SAT 2016)
Computing Maximum Unavoidable Subgraphs using SAT Solvers
graph width measures
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
H
Hash functions
(POS-16)
Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions
history map
(POS-16)
Approximate History Map for Massively Parallel Environments
Horn formulas
(SAT 2016)
Strong Backdoors for Default Logic
I
implicit hitting set algorithms
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
implied constraints
(POS-16)
A Study on Implied Constraints in a MaxSAT Approach to B2B Problems
improve evaluation
(POS-16)
Better Evaluations by Analyzing Benchmark Structure
incidence graph
(STRUCTSAT 2016)
Complexity and Approximability for Parameterized MAXCSPs
incremental MaxSAT
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
irreducible clause-sets
(STRUCTSAT 2016)
Minimal unsatisfiability and deficiency: recent developments
Isomorphism
(SAT 2016)
Solution-Graphs of Boolean Formulas and Isomorphism
K
knowledge compilation
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
(STRUCTSAT 2016)
Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas
Krom formulas
(SAT 2016)
Strong Backdoors for Default Logic
L
learning rate
(SAT 2016)
Learning Rate Based Branching Heuristic for SAT Solvers
lexicographic SAT (LEXSAT)
(SAT 2016)
Heuristic NPN classification for large functions using AIGs and LEXSAT
linear combinations
(SAT 2016)
Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
local search
(SAT 2016)
A SAT Approach to Branchwidth
(SAT 2016)
The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
logic synthesis
(SAT 2016)
Heuristic NPN classification for large functions using AIGs and LEXSAT
Long Distance Resolution
(SAT 2016)
Long Distance Q-Resolution with Dependency Schemes
long-distance resolution
(QBF 2016)
Dependency Schemes in QBF Calculi: Semantics and Soundness
lower bound
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
M
matrix symmetry
(SAT 2016)
Improved static symmetry breaking for SAT
Max SAT
(SAT 2016)
The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
(STRUCTSAT 2016)
CNF Encoding of Cardinality Constraints via Tree-Decomposition
Maximum satistiability
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
MaxSAT encodings
(POS-16)
A Study on Implied Constraints in a MaxSAT Approach to B2B Problems
MaxSAT solving
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
mcSAT
(SAT 2016)
Deciding Bit-Vector Formulas with mcSAT
MCSes
(SAT 2016)
BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
Median Graphs
(SAT 2016)
Solution-Graphs of Boolean Formulas and Isomorphism
Minimal Correction Subsets (MCSes)
(SAT 2016)
MCS Extraction with Sublinear Oracle Calls
minimal unsatisfiability
(STRUCTSAT 2016)
Minimal unsatisfiability and deficiency: recent developments
Minimal Unsatisfiable Subsets (MUSes)
(SAT 2016)
MCS Extraction with Sublinear Oracle Calls
model construction
(SAT 2016)
Deciding Bit-Vector Formulas with mcSAT
modular treewidth
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
modularity
(SAT 2016)
On the Hardness of SAT with Community Structure
multi-armed bandit learning
(SAT 2016)
Learning Rate Based Branching Heuristic for SAT Solvers
multi-sorted first-order logic
(SAT 2016)
Finding Finite Models in Multi-Sorted First Order Logic
MUSes
(SAT 2016)
BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
N
neighborhood diversity
(SAT 2016)
Parameterized Compilation Lower Bounds for Restricted CNF-formulas
non-prenex negation normal form
(SAT 2016)
Non-prenex QBF Solving using Abstraction
NPN classification
(SAT 2016)
Heuristic NPN classification for large functions using AIGs and LEXSAT
O
optimization
(SAT 2016)
Learning Rate Based Branching Heuristic for SAT Solvers
P
Parallel
(SAT 2016)
HordeQBF: A Modular and Massively Parallel QBF Solver
Parallel computing
(SAT 2016)
OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Parallel SAT solving
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
parallelization
(SAT 2016)
Non-prenex QBF Solving using Abstraction
Parameterised Complexity
(SAT 2016)
Strong Backdoors for Default Logic
parameterized complexity
(STRUCTSAT 2016)
Using Decomposition-Parameters for QBF: Mind the Prefix!
Partial Cube
(SAT 2016)
Solution-Graphs of Boolean Formulas and Isomorphism
Picture Languages
(SAT 2016)
Satisfiability via Smooth Pictures
polynomial simulation
(SAT 2016)
On stronger calculi for QBFs
polyomino
(QBF 2016)
QBF Encoding of Generalized Tic-Tac-Toe
predicate elimination
(SAT 2016)
Predicate elimination for preprocessing in first-order theorem proving
preprocessing
(SAT 2016)
Predicate elimination for preprocessing in first-order theorem proving
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
Program analysis
(SAT 2016)
Speeding Up the Constraint-Based Method in Difference Logic
program synthesis
(SAT 2016)
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
proof complexity
(POS-16)
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
(SAT 2016)
Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
(SAT 2016)
On the Hardness of SAT with Community Structure
proof system
(SAT 2016)
On Q-Resolution and DPLL QBF Solving
proof systems
(SAT 2016)
Lifting QBF Resolution Calculi to DQBF
proof theory
(SAT 2016)
On stronger calculi for QBFs
propagation completeness
(SAT 2016)
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Propositional Formulas
(POS-16)
The Clashing-Neighbor Relation for Propositional Formulas
propositional model counting
(STRUCTSAT 2016)
Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas
pseudo-industrial instances
(STRUCTSAT 2016)
Pseudo-Industrial Random SAT Generators
PSPACE
(SAT 2016)
2QBF: challenges and solutions
Pythagorean Triples
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
Q
Q-Resolution
(SAT 2016)
On Q-Resolution and DPLL QBF Solving
(QBF 2016)
Dependency Schemes in QBF Calculi: Semantics and Soundness
QBF
(SAT 2016)
2QBF: challenges and solutions
(SAT 2016)
HordeQBF: A Modular and Massively Parallel QBF Solver
(SAT 2016)
On Q-Resolution and DPLL QBF Solving
(SAT 2016)
Lifting QBF Resolution Calculi to DQBF
QBF calculi
(QBF 2016)
Dependency Schemes in QBF Calculi: Semantics and Soundness
QBF encoding
(QBF 2016)
QBF Encoding of Generalized Tic-Tac-Toe
QBF solver
(QBF 2016)
Dynamic Programming-based QBF Solving
QCDCL
(SAT 2016)
Q-Resolution with Generalized Axioms
quantified bit-vectors
(SAT 2016)
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
quantified boolean formula
(SAT 2016)
Non-prenex QBF Solving using Abstraction
(STRUCTSAT 2016)
Using Decomposition-Parameters for QBF: Mind the Prefix!
Quantified Boolean formulas
(SAT 2016)
Q-Resolution with Generalized Axioms
(SAT 2016)
Dependency Schemes for DQBF
(SAT 2016)
On stronger calculi for QBFs
(SAT 2016)
Long Distance Q-Resolution with Dependency Schemes
(SAT 2016)
Incremental Determinization
R
Ramsey Theory
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
random SAT generation
(STRUCTSAT 2016)
Pseudo-Industrial Random SAT Generators
resolution
(SAT 2016)
Q-Resolution with Generalized Axioms
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
(SAT 2016)
Long Distance Q-Resolution with Dependency Schemes
(SAT 2016)
Lifting QBF Resolution Calculi to DQBF
resolution calculi for QBFs and first-order logic
(SAT 2016)
On stronger calculi for QBFs
row interchangeability
(SAT 2016)
Improved static symmetry breaking for SAT
S
SAT
(SAT 2016)
Extreme Cases in SAT Problems
(SAT 2016)
Incremental Determinization
SAT encoding
(SAT 2016)
A SAT Approach to Branchwidth
SAT encodings
(SAT 2016)
Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
SAT Oracles
(SAT 2016)
MCS Extraction with Sublinear Oracle Calls
SAT solvers
(POS-16)
Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions
SAT solving
(SAT 2016)
Computing Maximum Unavoidable Subgraphs using SAT Solvers
Satisfiability
(SAT 2016)
Satisfiability via Smooth Pictures
(STRUCTSAT 2016)
Using Decomposition-Parameters for QBF: Mind the Prefix!
Satisfiability Testing
(SAT 2016)
SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
search space
(POS-16)
Approximate History Map for Massively Parallel Environments
shatter
(SAT 2016)
Improved static symmetry breaking for SAT
simulation
(SAT 2016)
On Q-Resolution and DPLL QBF Solving
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
size
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
Skolem functions
(SAT 2016)
Incremental Determinization
Smooth Pictures
(SAT 2016)
Satisfiability via Smooth Pictures
SMT
(SAT 2016)
Deciding Bit-Vector Formulas with mcSAT
(SAT 2016)
Speeding Up the Constraint-Based Method in Difference Logic
SMT solvers
(SAT 2016)
OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
smt solving
(SAT 2016)
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
solution enumeration
(SAT 2016)
LMHS: A SAT-IP Hybrid MaxSAT Solver
Solver
(SAT 2016)
HordeQBF: A Modular and Massively Parallel QBF Solver
solver evaluation
(POS-16)
Better Evaluations by Analyzing Benchmark Structure
space
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
splitting
(SAT 2016)
Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
stabilizer chain
(SAT 2016)
Improved static symmetry breaking for SAT
static symmetry breaking
(SAT 2016)
Improved static symmetry breaking for SAT
Strategy Extraction
(SAT 2016)
Long Distance Q-Resolution with Dependency Schemes
structural parameterizations
(STRUCTSAT 2016)
Complexity and Approximability for Parameterized MAXCSPs
structure-based algorithm
(STRUCTSAT 2016)
Structure-based knowledge compilation: the singular case of $\beta$-acyclic formulas
Succinct
(SAT 2016)
Solution-Graphs of Boolean Formulas and Isomorphism
symmetry
(SAT 2016)
Improved static symmetry breaking for SAT
symmetry breaking
(SAT 2016)
Computing Maximum Unavoidable Subgraphs using SAT Solvers
symmetry breaking predicates
(SAT 2016)
Improved static symmetry breaking for SAT
Synthesis
(SAT 2016)
2QBF: challenges and solutions
(SAT 2016)
Incremental Determinization
T
Theoretical benchmarks
(POS-16)
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks
trade-offs
(SAT 2016)
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
tree decomposition
(QBF 2016)
Dynamic Programming-based QBF Solving
tree-decomposition
(STRUCTSAT 2016)
CNF Encoding of Cardinality Constraints via Tree-Decomposition
Treewidth
(STRUCTSAT 2016)
Experiments with CNF Structure and Hardness
treewidth and pathwidth
(STRUCTSAT 2016)
Using Decomposition-Parameters for QBF: Mind the Prefix!
V
vampire
(SAT 2016)
Finding Finite Models in Multi-Sorted First Order Logic
variable degrees
(STRUCTSAT 2016)
Minimal unsatisfiability and deficiency: recent developments
verification
(SAT 2016)
2QBF: challenges and solutions
(SAT 2016)
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
VSIDS
(STRUCTSAT 2016)
Experiments with CNF Structure and Hardness