SAT 2015: 18TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

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

#
#sat	Laissez-Faire Caching for Parallel #SAT Solving
A
AIG	Recognition of Nested Gates in CNF Formulas
algorithm configuration	SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Algorithm Portfolios	Search-Space Partitioning for Parallelizing SMT Solvers
assumptions	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
autarky	Computing maximal autarkies with few and simple oracle queries
autarky-resolution duality	Computing maximal autarkies with few and simple oracle queries
Axiom pinpointing	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
B
BCD	Recognition of Nested Gates in CNF Formulas
BCE	Recognition of Nested Gates in CNF Formulas
blocked clause elimination	Preprocessing for DQBF
Blocked Set	Recognition of Nested Gates in CNF Formulas
Boolean Satisfiability	Speeding up MUS Extraction with Preprocessing and Chunking
BVA	Recognition of Nested Gates in CNF Formulas
BVE	Recognition of Nested Gates in CNF Formulas
C
CDCL	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
Clause Learning	Using Community Structure to Detect Relevant Learnt Clauses
Clauses	Hints Revealed
Cloud computing	Search-Space Partitioning for Parallelizing SMT Solvers
Cluster	HordeSat: A Massively Parallel Portfolio SAT Solver
CNF	Recognition of Nested Gates in CNF Formulas
CNF/DNF formula minimization	SAT-Based Formula Simplification
cnf2aig	Recognition of Nested Gates in CNF Formulas
COMiniSatPS	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
community structure	Using Community Structure to Detect Relevant Learnt Clauses Community Structure Inspired Algorithms for SAT and #SAT SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
Configuration checking	CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
constraint satisfaction problem	Constructing SAT filters with a quantum annealer
D
decision heuristics	Evaluating CDCL Variable Scoring Schemes
Deterministic DNNFs	On Compiling CNFs into Structured Deterministic DNNFs
Divide and Conquer	Search-Space Partitioning for Parallelizing SMT Solvers
DQBF	Preprocessing for DQBF
E
Encoding	PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
F
fixed-parameter tractability	Community Structure Inspired Algorithms for SAT and #SAT
Forgetting	Projected Model Counting
framework	Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
G
Gate Detection	Recognition of Nested Gates in CNF Formulas
Graph Representations	Exploiting Resolution-based Representations for MaxSAT Solving
Group-MUS enumeration	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
H
hitting formulas	Community Structure Inspired Algorithms for SAT and #SAT
Horn formulae	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
Horn least upper bounds	SAT-Based Horn Least Upper Bounds
I
identify clause blocks	A New Approach to Partial MUS Enumeration
incremental SAT	Mining Implied Literals for Incremental SAT
incremental solving	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Ising model	Constructing SAT filters with a quantum annealer
K
Knowledge Compilation	On Compiling CNFs into Structured Deterministic DNNFs
Knowledge compilation and approximation	SAT-Based Horn Least Upper Bounds
L
laissez-faire caching	Laissez-Faire Caching for Parallel #SAT Solving
large maxsat instances	Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
lazy grounding	Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
learned clause	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
learning	QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
levelized SAT solving	QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
linear-time analysis	Mining Implied Literals for Incremental SAT
Local search	CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
M
MAX-k-CSP	Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
MAX-SAT	Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
maximal autarky	Computing maximal autarkies with few and simple oracle queries
maximum cut	Constructing SAT filters with a quantum annealer
Maximum Satisfiability	Exploiting Resolution-based Representations for MaxSAT Solving
minimal unsatisfiability	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Minimal Unsatisfiable Cores	Speeding up MUS Extraction with Preprocessing and Chunking
minimal unsatisfiable subsets	A New Approach to Partial MUS Enumeration
MiniSat	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
model counting	Projected Model Counting Community Structure Inspired Algorithms for SAT and #SAT
N
Non-clausal formula simplification	SAT-Based Formula Simplification
Non-linear real and integer arithmetic	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
O
oracles	Computing maximal autarkies with few and simple oracle queries
P
Parallel	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving HordeSat: A Massively Parallel Portfolio SAT Solver
Parallel computing	Search-Space Partitioning for Parallelizing SMT Solvers
parallelization	Laissez-Faire Caching for Parallel #SAT Solving
parameter importance	SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
parameterized complexity	Community Structure Inspired Algorithms for SAT and #SAT
partial MUS enumeration	A New Approach to Partial MUS Enumeration
Partial resolution	Hints Revealed
performance analysis	SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Portfolio	HordeSat: A Massively Parallel Portfolio SAT Solver
practical analysis	A New Approach to Partial MUS Enumeration
Preprocessing	Speeding up MUS Extraction with Preprocessing and Chunking Preprocessing for DQBF Recognition of Nested Gates in CNF Formulas
Projection	Projected Model Counting
propositional satisfiability	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
Pseudo-Boolean	PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Q
QBF	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
QF_UF theory	Search-Space Partitioning for Parallelizing SMT Solvers
quantified Boolean formula	QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
quantum annealing	Constructing SAT filters with a quantum annealer
Quine-McCluskey procedure pure SAT-based	SAT-Based Formula Simplification
R
Resolution	Hints Revealed
resolution proof analysis	Mining Implied Literals for Incremental SAT
restart	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
S
sampling	Constructing SAT filters with a quantum annealer
SAT	Evaluating CDCL Variable Scoring Schemes Community Structure Inspired Algorithms for SAT and #SAT Between SAT and UNSAT: The Fundamental Difference in CDCL SAT SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
SAT filter	Constructing SAT filters with a quantum annealer
SAT solver	CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
SAT solvers	Using Community Structure to Detect Relevant Learnt Clauses
SAT translation	Computing maximal autarkies with few and simple oracle queries
SAT-based algorithms	SAT-Based Horn Least Upper Bounds
Satisfiability	HordeSat: A Massively Parallel Portfolio SAT Solver
satisfiability algorithm	Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
Satisfiability proving	Hints Revealed
shared memory	Laissez-Faire Caching for Parallel #SAT Solving
SMT	Search-Space Partitioning for Parallelizing SMT Solvers
SMT solving	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Strategic	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Structure	Recognition of Nested Gates in CNF Formulas
Structured CNFs	On Compiling CNFs into Structured Deterministic DNNFs
Stuctured instances	CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
sum of products	Community Structure Inspired Algorithms for SAT and #SAT
SWDiA5BY	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
T
Tool	PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Toolbox	SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
treewidth	Community Structure Inspired Algorithms for SAT and #SAT
U
Unsat core	Hints Revealed
UNSAT proof	Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
unsatisfiability	A New Approach to Partial MUS Enumeration
Unsatisfiability-based solvers	Exploiting Resolution-based Representations for MaxSAT Solving
unsatisfiable core	Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
V
visualisation	SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
VMTF	Evaluating CDCL Variable Scoring Schemes
VSIDS	Evaluating CDCL Variable Scoring Schemes Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
W
workload	A New Approach to Partial MUS Enumeration

Disclaimer | Powered by EasyChair Smart Program