SAT 2016: 19TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

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

2
2QBF	Incremental Determinization
A
And-inverter graphs (AIGs)	Heuristic NPN classification for large functions using AIGs and LEXSAT
approximation	Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
auto tuning	Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Autocorrelation Length	The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
Automated Configuration	SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
average-case hardness	On the Hardness of SAT with Community Structure
Axiom pinpointing	BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
axioms	Q-Resolution with Generalized Axioms
B
Backdoors	Strong Backdoors for Default Logic
binary decision diagrams	Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
bit-vectors	Deciding Bit-Vector Formulas with mcSAT
Blackbox Fuzz Testing	SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
branch decomposition	A SAT Approach to Branchwidth
Branching	Extreme Cases in SAT Problems
branching heuristic	Learning Rate Based Branching Heuristic for SAT Solvers
C
CDCL	Extreme Cases in SAT Problems Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
cegar	2QBF: challenges and solutions Non-prenex QBF Solving using Abstraction
Certificates	Incremental Determinization
clause learning	Q-Resolution with Generalized Axioms
Cloud computing	OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Combinatorial Optimization	The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
combinatorics	Computing Maximum Unavoidable Subgraphs using SAT Solvers
Community Structure	On the Hardness of SAT with Community Structure
conflict-driven clause learning	Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
conflict-driven clause learning solvers	On the Hardness of SAT with Community Structure
conflict-driven clause-learning	Learning Rate Based Branching Heuristic for SAT Solvers
Counting	Solution-Graphs of Boolean Formulas and Isomorphism
cube learning	Q-Resolution with Generalized Axioms
Cube-and-conquer	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
D
decomposable negation normal form	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
Default Logic	Strong Backdoors for Default Logic
dependency schemes	Dependency Schemes for DQBF Long Distance Q-Resolution with Dependency Schemes
Difference Logic	Speeding Up the Constraint-Based Method in Difference Logic
DPLL	Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
DQBF	Dependency Schemes for DQBF Lifting QBF Resolution Calculi to DQBF
DRAT proofs	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
E
Encoding	Speeding Up the Constraint-Based Method in Difference Logic
F
finite model building	Finding Finite Models in Multi-Sorted First Order Logic
finite model finding	Finding Finite Models in Multi-Sorted First Order Logic
first-order theorem proving	Predicate elimination for preprocessing in first-order theorem proving
Fitness Landscape	The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
G
generating explanations	Deciding Bit-Vector Formulas with mcSAT
graph theory	Computing Maximum Unavoidable Subgraphs using SAT Solvers
graph width measures	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
H
Horn formulas	Strong Backdoors for Default Logic
I
implicit hitting set algorithms	LMHS: A SAT-IP Hybrid MaxSAT Solver
incremental MaxSAT	LMHS: A SAT-IP Hybrid MaxSAT Solver
Isomorphism	Solution-Graphs of Boolean Formulas and Isomorphism
K
knowledge compilation	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
Krom formulas	Strong Backdoors for Default Logic
L
learning rate	Learning Rate Based Branching Heuristic for SAT Solvers
lexicographic SAT (LEXSAT)	Heuristic NPN classification for large functions using AIGs and LEXSAT
linear combinations	Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
local search	A SAT Approach to Branchwidth The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
logic synthesis	Heuristic NPN classification for large functions using AIGs and LEXSAT
Long Distance Resolution	Long Distance Q-Resolution with Dependency Schemes
lower bound	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
M
matrix symmetry	Improved static symmetry breaking for SAT
Max SAT	The Normalized Autocorrelation Length of Random Max r-Sat Converges in Probability to (1-1/2^r)/r
Maximum satistiability	LMHS: A SAT-IP Hybrid MaxSAT Solver
MaxSAT solving	LMHS: A SAT-IP Hybrid MaxSAT Solver
mcSAT	Deciding Bit-Vector Formulas with mcSAT
MCSes	BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
Median Graphs	Solution-Graphs of Boolean Formulas and Isomorphism
Minimal Correction Subsets (MCSes)	MCS Extraction with Sublinear Oracle Calls
Minimal Unsatisfiable Subsets (MUSes)	MCS Extraction with Sublinear Oracle Calls
model construction	Deciding Bit-Vector Formulas with mcSAT
modular treewidth	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
modularity	On the Hardness of SAT with Community Structure
multi-armed bandit learning	Learning Rate Based Branching Heuristic for SAT Solvers
multi-sorted first-order logic	Finding Finite Models in Multi-Sorted First Order Logic
MUSes	BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies
N
neighborhood diversity	Parameterized Compilation Lower Bounds for Restricted CNF-formulas
non-prenex negation normal form	Non-prenex QBF Solving using Abstraction
NPN classification	Heuristic NPN classification for large functions using AIGs and LEXSAT
O
optimization	Learning Rate Based Branching Heuristic for SAT Solvers
P
Parallel	HordeQBF: A Modular and Massively Parallel QBF Solver
Parallel computing	OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
Parallel SAT solving	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
parallelization	Non-prenex QBF Solving using Abstraction
Parameterised Complexity	Strong Backdoors for Default Logic
Partial Cube	Solution-Graphs of Boolean Formulas and Isomorphism
Picture Languages	Satisfiability via Smooth Pictures
polynomial simulation	On stronger calculi for QBFs
predicate elimination	Predicate elimination for preprocessing in first-order theorem proving
preprocessing	Predicate elimination for preprocessing in first-order theorem proving LMHS: A SAT-IP Hybrid MaxSAT Solver
Program analysis	Speeding Up the Constraint-Based Method in Difference Logic
program synthesis	Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
proof complexity	Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle On the Hardness of SAT with Community Structure
proof system	On Q-Resolution and DPLL QBF Solving
proof systems	Lifting QBF Resolution Calculi to DQBF
proof theory	On stronger calculi for QBFs
propagation completeness	Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
PSPACE	2QBF: challenges and solutions
Pythagorean Triples	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
Q
Q-Resolution	On Q-Resolution and DPLL QBF Solving
QBF	2QBF: challenges and solutions HordeQBF: A Modular and Massively Parallel QBF Solver On Q-Resolution and DPLL QBF Solving Lifting QBF Resolution Calculi to DQBF
QCDCL	Q-Resolution with Generalized Axioms
quantified bit-vectors	Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
quantified boolean formula	Non-prenex QBF Solving using Abstraction
Quantified Boolean formulas	Q-Resolution with Generalized Axioms Dependency Schemes for DQBF On stronger calculi for QBFs Long Distance Q-Resolution with Dependency Schemes Incremental Determinization
R
Ramsey Theory	Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
resolution	Q-Resolution with Generalized Axioms Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers Long Distance Q-Resolution with Dependency Schemes Lifting QBF Resolution Calculi to DQBF
resolution calculi for QBFs and first-order logic	On stronger calculi for QBFs
row interchangeability	Improved static symmetry breaking for SAT
S
SAT	Extreme Cases in SAT Problems Incremental Determinization
SAT encoding	A SAT Approach to Branchwidth
SAT encodings	Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
SAT Oracles	MCS Extraction with Sublinear Oracle Calls
SAT solving	Computing Maximum Unavoidable Subgraphs using SAT Solvers
Satisfiability	Satisfiability via Smooth Pictures
Satisfiability Testing	SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers
shatter	Improved static symmetry breaking for SAT
simulation	On Q-Resolution and DPLL QBF Solving Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
size	Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
Skolem functions	Incremental Determinization
Smooth Pictures	Satisfiability via Smooth Pictures
SMT	Deciding Bit-Vector Formulas with mcSAT Speeding Up the Constraint-Based Method in Difference Logic
SMT solvers	OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing
smt solving	Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
solution enumeration	LMHS: A SAT-IP Hybrid MaxSAT Solver
Solver	HordeQBF: A Modular and Massively Parallel QBF Solver
space	Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
splitting	Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle
stabilizer chain	Improved static symmetry breaking for SAT
static symmetry breaking	Improved static symmetry breaking for SAT
Strategy Extraction	Long Distance Q-Resolution with Dependency Schemes
Succinct	Solution-Graphs of Boolean Formulas and Isomorphism
symmetry	Improved static symmetry breaking for SAT
symmetry breaking	Computing Maximum Unavoidable Subgraphs using SAT Solvers
symmetry breaking predicates	Improved static symmetry breaking for SAT
Synthesis	2QBF: challenges and solutions Incremental Determinization
T
trade-offs	Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
V
vampire	Finding Finite Models in Multi-Sorted First Order Logic
verification	2QBF: challenges and solutions Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

Disclaimer | Powered by EasyChair Smart Program