VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

A
application	Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
approximation	Approximating highly satisfiable random 2-SAT
assumptions	MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
B
Betweenness centrality	Impact of Community Structure on SAT Solver Performance
Blocked Clause Decomposition	Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
Blocked Sets	Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
C
cardinality constraints	Detecting cardinality constraints in CNF
CDCL	Long Proofs of (Seemingly) Simple Formulas
CDCL solvers	Impact of Community Structure on SAT Solver Performance
Chinese Remainder Theorem	Simplifying Pseudo-Boolean Constraints in Residual Number Systems
clausal proofs	MUS Extraction using Clausal Proofs
combinatorial topology	Proof complexity and the Lovasz-Kneser Theorem
Community detection	Community Branching for Parallel Portfolio SAT Solvers
Community Structure	Impact of Community Structure on SAT Solver Performance
complexity analysis	Fixed-parameter tractable reductions to SAT
Condensed-matter physics	An Ising Model inspired Extension of the Product-based MP Framework for SAT
Controllability	Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
cores	Cores in Core based MaxSat Algorithms: an Analysis
counting	Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
D
Decision	Community Branching for Parallel Portfolio SAT Solvers
degree	Long Proofs of (Seemingly) Simple Formulas
Dependency Schemes	Variable Dependencies and Q-Resolution
Diversification	Community Branching for Parallel Portfolio SAT Solvers
DNF minimization	Fixed-parameter tractable reductions to SAT
DQBF solving	Fast DQBF Refutation
dynamic programming	Solving MaxSAT and #SAT on structured CNF formulas
E
Experimental mathematics	A SAT Attack on the Erdos Discrepancy Conjecture
exponential time algorithm	Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
Extended resolution	DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
F
failed literal detection	Conditional Lower Bounds for Failed Literals and Related Techniques
Forms of agitation	An Ising Model inspired Extension of the Product-based MP Framework for SAT
formula trimming	DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
Frege proofs	Proof complexity and the Lovasz-Kneser Theorem
G
game characterisations	Unified characterisations of resolution hardness measures
H
hard constraint	Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
hard SAT instances	Long Proofs of (Seemingly) Simple Formulas
hardness	Unified characterisations of resolution hardness measures
hardness results	Fixed-parameter tractable reductions to SAT
Hypergraph decomposition	Hypergraph Acyclicity and Propositional Model Counting
I
Implementation Techniques	Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
implicant minimization	Fixed-parameter tractable reductions to SAT
incomplete information	Fast DQBF Refutation
Incremental Preprocessing	Ultimately Incremental SAT
Incremental SAT	Ultimately Incremental SAT
Integrating CDCL and MP	An Ising Model inspired Extension of the Product-based MP Framework for SAT
Ising Model	An Ising Model inspired Extension of the Product-based MP Framework for SAT
K
k-SAT	Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
L
length	Long Proofs of (Seemingly) Simple Formulas
lower bound	Long Proofs of (Seemingly) Simple Formulas
lower bounds	Conditional Lower Bounds for Failed Literals and Related Techniques
M
max-2-sat	Approximating highly satisfiable random 2-SAT
Max-SMT	Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
Maximal Satisfiable Subsets	On Computing Preferred MUSes and MCSes
Maximum Falsifiability	On Reducing Maximum Independent Set to Minimum Satisfiability
Maximum Independent Set	On Reducing Maximum Independent Set to Minimum Satisfiability
Maximum satisfiability	Open-WBO: a Modular MaxSAT Solver Approximating highly satisfiable random 2-SAT
MaxSAT	Cores in Core based MaxSat Algorithms: an Analysis Solving MaxSAT and #SAT on structured CNF formulas
Message Passing	An Ising Model inspired Extension of the Product-based MP Framework for SAT
Minimal Correction Subsets	On Computing Preferred MUSes and MCSes
Minimal Unsatisfiable Core	MUS Extraction using Clausal Proofs
Minimal Unsatisfiable Subsets	On Computing Preferred MUSes and MCSes
Minimum Satisfiability	On Reducing Maximum Independent Set to Minimum Satisfiability
Minisat	Ultimately Incremental SAT
model counting	Solving MaxSAT and #SAT on structured CNF formulas
Modular Solver	Open-WBO: a Modular MaxSAT Solver
N
NP-completeness	Automatic Evaluation of Reductions between NP-complete Problems
O
Open-Source	Open-WBO: a Modular MaxSAT Solver
P
Parallel	MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing Lazy clause exchange policy for parallel SAT solvers
Parallel SAT solver	Community Branching for Parallel Portfolio SAT Solvers
parameterized complexity	Fixed-parameter tractable reductions to SAT
partial equivalence checking problem	Fast DQBF Refutation
PCR	Long Proofs of (Seemingly) Simple Formulas
planted distribution	Approximating highly satisfiable random 2-SAT
polynomial calculus	Long Proofs of (Seemingly) Simple Formulas
Polynomial Contraints	Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
Polynomial Hierarchy	Fixed-parameter tractable reductions to SAT
polynomial space	Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
polynomial time algorithm	Solving MaxSAT and #SAT on structured CNF formulas
Portfolio	Community Branching for Parallel Portfolio SAT Solvers
Power managment designs	Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
preferences	On Computing Preferred MUSes and MCSes
preprocessing	Conditional Lower Bounds for Failed Literals and Related Techniques Detecting cardinality constraints in CNF
proof checking	DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
proof complexity	QBF Resolution Systems and their Proof Complexities Unified characterisations of resolution hardness measures
Propositional model counting	Hypergraph Acyclicity and Propositional Model Counting
pseudo-Boolean Constraints	Simplifying Pseudo-Boolean Constraints in Residual Number Systems
Q
Q-resolution	Variable Dependencies and Q-Resolution
QBF	MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
QBF of bounded treewidth	Fixed-parameter tractable reductions to SAT
QBF-solver	Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
quantified Boolean formula	QBF Resolution Systems and their Proof Complexities
Quantified Boolean Formulas	Variable Dependencies and Q-Resolution
R
random satisfiability	Approximating highly satisfiable random 2-SAT
Reductions	Automatic Evaluation of Reductions between NP-complete Problems
residual number system	Simplifying Pseudo-Boolean Constraints in Residual Number Systems
resolution	QBF Resolution Systems and their Proof Complexities Long Proofs of (Seemingly) Simple Formulas Unified characterisations of resolution hardness measures
resolution complexity	Proof complexity and the Lovasz-Kneser Theorem
resolution space	Unified characterisations of resolution hardness measures
resolution width	Unified characterisations of resolution hardness measures
S
SAT	Unified characterisations of resolution hardness measures Lazy clause exchange policy for parallel SAT solvers
SAT application	Automatic Evaluation of Reductions between NP-complete Problems
SAT encoding of combinatorial problems	A SAT Attack on the Erdos Discrepancy Conjecture
sat encodings	Detecting cardinality constraints in CNF
SAT under Assumptions	Ultimately Incremental SAT
SatELite	Ultimately Incremental SAT
satisfiability	Conditional Lower Bounds for Failed Literals and Related Techniques Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
Self-learning	Automatic Evaluation of Reductions between NP-complete Problems
sequence of sat	Cores in Core based MaxSat Algorithms: an Analysis
Sequences of small discrepancy	A SAT Attack on the Erdos Discrepancy Conjecture
singleton arc consistency	Conditional Lower Bounds for Failed Literals and Related Techniques
size	Long Proofs of (Seemingly) Simple Formulas
Skolem/Herbrand function	QBF Resolution Systems and their Proof Complexities
SLS	Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
SMT	Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
Solver	Lazy clause exchange policy for parallel SAT solvers
solving	MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
Special cases of MP	An Ising Model inspired Extension of the Product-based MP Framework for SAT
Structural tractability	Hypergraph Acyclicity and Propositional Model Counting
System description	DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
T
trimming	MUS Extraction using Clausal Proofs
V
verification	Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
W
weight	Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
width	Long Proofs of (Seemingly) Simple Formulas

Disclaimer | Powered by EasyChair Smart Program