Theory and Application of Satisfiability Testing: 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011, Proceedings

Front Matter....Pages -
Connecting SAT Algorithms and Complexity Lower Bounds....Pages 1-2
Concolic Testing and Constraint Satisfaction....Pages 3-4
Minimally Unsatisfiable Boolean Circuits....Pages 145-158
On Improving MUS Extraction Algorithms....Pages 159-173
Faster Extraction of High-Level Minimal Unsatisfiable Cores....Pages 174-187
On Freezing and Reactivating Learnt Clauses....Pages 188-200
Efficient CNF Simplification Based on Binary Implication Graphs....Pages 201-215
Between Restarts and Backjumps....Pages 216-229
Abstraction-Based Algorithm for 2QBF....Pages 230-244
Transformations into Normal Forms for Quantified Circuits....Pages 245-258
Parameterized Complexity of DPLL Search Procedures....Pages 5-18
Satisfiability Certificates Verifiable in Subexponential Time....Pages 19-32
On Variables with Few Occurrences in Conjunctive Normal Forms....Pages 33-46
Satisfiability of Acyclic and almost Acyclic CNF Formulas (II)....Pages 47-60
BDDs for Pseudo-Boolean Constraints – Revisited....Pages 61-75
DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions....Pages 76-89
 π DD: A New Decision Diagram for Efficient Problem Solving in Permutation Space....Pages 90-104
How to Apply SAT-Solving for the Equivalence Test of Monotone Normal Forms....Pages 105-119
Enumerating All Solutions of a Boolean CSP by Non-decreasing Weight....Pages 120-133
A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs....Pages 134-144
Failed Literal Detection for QBF....Pages 259-272
Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One....Pages 273-286
Generating Diverse Solutions in SAT....Pages 287-301
Captain Jack: New Variable Selection Heuristics in Local Search for SAT....Pages 302-316
Careful Ranking of Multiple Solvers with Timeouts and Ties....Pages 317-328
Generalized Conflict-Clause Strengthening for Satisfiability Solvers....Pages 329-342
Empirical Study of the Anatomy of Modern Sat Solvers....Pages 343-356
Translating Pseudo-Boolean Constraints into CNF....Pages 357-359
Analyzing the Instances of the MaxSAT Evaluation....Pages 360-361
Model Counting Using the Inclusion-Exclusion Principle....Pages 362-363
Phase Transitions in Knowledge Compilation: An Experimental Study....Pages 364-366
EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation....Pages 367-368
Non-Model-Based Algorithm Portfolios for SAT....Pages 369-370
The Order Encoding: From Tractable CSP to Tractable SAT....Pages 371-372
Applying UCT to Boolean Satisfiability....Pages 373-374
A Compact and Efficient SAT-Encoding of Finite Domain CSP....Pages 375-376
Learning Polarity from Structure in SAT....Pages 377-378
Back Matter....Pages -