Theory and Applications of Satisfiability Testing - SAT 2014 [electronic resource] : 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings / edited by Carsten Sinz, Uwe Egly.

A (Biased) Proof Complexity Survey for SAT Practitioners -- Cores in Core Based MaxSat Algorithms: An Analysis -- Solving MaxSAT and #SAT on Structured CNF Formulas -- Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction -- MUS Extraction Using Clausal Proofs -- On Computing Preferred MUSes and MCSes -- Conditional Lower Bounds for Failed Literals and Related Techniques -- Fixed-Parameter Tractable Reductions to SAT -- On Reducing Maximum Independent Set to Minimum Satisfiability -- Long Proofs of (Seemingly) Simple Formulas -- Proof Complexity and the Kneser-Lovász Theorem -- QBF Resolution Systems and Their Proof Complexities -- Unified Characterisations of Resolution Hardness Measures -- Community Branching for Parallel Portfolio SAT Solvers -- Lazy Clause Exchange Policy for Parallel SAT Solvers -- Ultimately Incremental SAT -- A SAT Attack on the Erdos Discrepancy Conjecture -- Dominant Controllability Check Using QBF-Solver and Netlist -- Fast DQBF Refutation -- Impact of Community Structure on SAT Solver Performance -- Variable Dependencies and Q-Resolution -- Detecting Cardinality Constraints in CNF -- Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses -- Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask) -- Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions -- Simplifying Pseudo-Boolean Constraints in Residual Number Systems -- An Ising Model Inspired Extension of the Product-Based MP Framework for SAT -- Approximating Highly Satisfiable Random 2-SAT -- Hypergraph Acyclicity and Propositional Model Counting -- Automatic Evaluation of Reductions between NP-Complete Problems -- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs -- MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing -- Open-WBO: A Modular MaxSAT Solver.