Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Theory and Applications of Satisfiability Testing - SAT 2009 [[electronic resource] ] : 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings / / edited by Oliver Kullmann
| Theory and Applications of Satisfiability Testing - SAT 2009 [[electronic resource] ] : 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings / / edited by Oliver Kullmann |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XII, 540 p.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Algorithms Operating systems (Computers) Numerical analysis Artificial intelligence Mathematical logic Formal Languages and Automata Theory Operating Systems Numerical Analysis Artificial Intelligence Mathematical Logic and Foundations |
| ISBN |
1-280-00000-7
9786613560995 3-642-02777-6 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms -- Symbolic Techniques in Propositional Satisfiability Solving -- Applications of SAT -- Efficiently Calculating Evolutionary Tree Measures Using SAT -- Finding Lean Induced Cycles in Binary Hypercubes -- Finding Efficient Circuits Using SAT-Solvers -- Encoding Treewidth into SAT -- Complexity Theory -- The Complexity of Reasoning for Fragments of Default Logic -- Does Advice Help to Prove Propositional Tautologies? -- Structures for SAT -- Backdoors in the Context of Learning -- Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences -- On Some Aspects of Mixed Horn Formulas -- Variable Influences in Conjunctive Normal Forms -- Resolution and SAT -- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution -- An Exponential Lower Bound for Width-Restricted Clause Learning -- Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces -- Boundary Points and Resolution -- Translations to CNF -- Sequential Encodings from Max-CSP into Partial Max-SAT -- Cardinality Networks and Their Applications -- New Encodings of Pseudo-Boolean Constraints into CNF -- Efficient Term-ITE Conversion for Satisfiability Modulo Theories -- Techniques for Conflict-Driven SAT Solvers -- On-the-Fly Clause Improvement -- Dynamic Symmetry Breaking by Simulating Zykov Contraction -- Minimizing Learned Clauses -- Extending SAT Solvers to Cryptographic Problems -- Solving SAT by Local Search -- Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability -- A Theoretical Analysis of Search in GSAT -- The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT -- Hybrid SAT Solvers -- A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem -- Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques -- Automatic Adaption of SAT Solvers -- Restart Strategy Selection Using Machine Learning Techniques -- Instance-Based Selection of Policies for SAT Solvers -- Width-Based Restart Policies for Clause-Learning Satisfiability Solvers -- Problem-Sensitive Restart Heuristics for the DPLL Procedure -- Stochastic Approaches to SAT Solving -- (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms -- VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search -- QBFs and Their Representations -- Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits -- A Compact Representation for Syntactic Dependencies in QBFs -- Beyond CNF: A Circuit-Based QBF Solver -- Optimisation Algorithms -- Solving (Weighted) Partial MaxSAT through Satisfiability Testing -- Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation? -- Relaxed DPLL Search for MaxSAT -- Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates -- Exploiting Cycle Structures in Max-SAT -- Generalizing Core-Guided Max-SAT -- Algorithms for Weighted Boolean Optimization -- Distributed and Parallel Solving -- PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing -- c-sat: A Parallel SAT Solver for Clusters. |
| Record Nr. | UNISA-996465588503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theory and applications of satisfiability testing - SAT 2009 : 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009 : proceedings / / Oliver Kullmann (ed.)
| Theory and applications of satisfiability testing - SAT 2009 : 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009 : proceedings / / Oliver Kullmann (ed.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2009 |
| Descrizione fisica | 1 online resource (XII, 540 p.) |
| Disciplina | 005.131 |
| Altri autori (Persone) | KullmannOliver |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Algebra, Boolean
Computer algorithms Decision making Propositional calculus |
| ISBN |
1-280-00000-7
9786613560995 3-642-02777-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms -- Symbolic Techniques in Propositional Satisfiability Solving -- Applications of SAT -- Efficiently Calculating Evolutionary Tree Measures Using SAT -- Finding Lean Induced Cycles in Binary Hypercubes -- Finding Efficient Circuits Using SAT-Solvers -- Encoding Treewidth into SAT -- Complexity Theory -- The Complexity of Reasoning for Fragments of Default Logic -- Does Advice Help to Prove Propositional Tautologies? -- Structures for SAT -- Backdoors in the Context of Learning -- Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences -- On Some Aspects of Mixed Horn Formulas -- Variable Influences in Conjunctive Normal Forms -- Resolution and SAT -- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution -- An Exponential Lower Bound for Width-Restricted Clause Learning -- Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces -- Boundary Points and Resolution -- Translations to CNF -- Sequential Encodings from Max-CSP into Partial Max-SAT -- Cardinality Networks and Their Applications -- New Encodings of Pseudo-Boolean Constraints into CNF -- Efficient Term-ITE Conversion for Satisfiability Modulo Theories -- Techniques for Conflict-Driven SAT Solvers -- On-the-Fly Clause Improvement -- Dynamic Symmetry Breaking by Simulating Zykov Contraction -- Minimizing Learned Clauses -- Extending SAT Solvers to Cryptographic Problems -- Solving SAT by Local Search -- Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability -- A Theoretical Analysis of Search in GSAT -- The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT -- Hybrid SAT Solvers -- A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem -- Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques -- Automatic Adaption of SAT Solvers -- Restart Strategy Selection Using Machine Learning Techniques -- Instance-Based Selection of Policies for SAT Solvers -- Width-Based Restart Policies for Clause-Learning Satisfiability Solvers -- Problem-Sensitive Restart Heuristics for the DPLL Procedure -- Stochastic Approaches to SAT Solving -- (1,2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms -- VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search -- QBFs and Their Representations -- Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits -- A Compact Representation for Syntactic Dependencies in QBFs -- Beyond CNF: A Circuit-Based QBF Solver -- Optimisation Algorithms -- Solving (Weighted) Partial MaxSAT through Satisfiability Testing -- Nonlinear Pseudo-Boolean Optimization: Relaxation or Propagation? -- Relaxed DPLL Search for MaxSAT -- Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates -- Exploiting Cycle Structures in Max-SAT -- Generalizing Core-Guided Max-SAT -- Algorithms for Weighted Boolean Optimization -- Distributed and Parallel Solving -- PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing -- c-sat: A Parallel SAT Solver for Clusters. |
| Altri titoli varianti | SAT 2009 |
| Record Nr. | UNINA-9910483934703321 |
| Berlin ; ; New York, : Springer, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||