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.
Classical propositional operators : an exercise in the foundations of logic / by Krister Segerberg
| Classical propositional operators : an exercise in the foundations of logic / by Krister Segerberg |
| Autore | Segerberg, Krister |
| Pubbl/distr/stampa | Oxford : Clarendon Press, 1982 |
| Descrizione fisica | x, 151 p. ; 24 cm. |
| Disciplina | 511.3 |
| Collana | Oxford logic guides ; 5 |
| Soggetto topico | Propositional calculus |
| ISBN | 0198531737 |
| Classificazione |
AMS 03B05
QA9.3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISALENTO-991000744789707536 |
Segerberg, Krister
|
||
| Oxford : Clarendon Press, 1982 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.]
| Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| Soggetto genere / forma | Electronic books. |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910455344403321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.]
| Handbook of satisfiability [[electronic resource] /] / edited by Armin Biere ... [et al.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Classificazione |
ST 125
ST 300 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910778077003321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Handbook of satisfiability / / edited by Armin Biere ... [et al.]
| Handbook of satisfiability / / edited by Armin Biere ... [et al.] |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 |
| Descrizione fisica | 1 online resource (980 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | BiereArmin |
| Collana | Frontiers in artificial intelligence and applications |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN |
1-4416-1678-0
1-60750-376-X 600-00-1439-2 |
| Classificazione |
ST 125
ST 300 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Title page; Contents; Part I. Theory and Algorithms; Chapter 1. A History of Satisfiability; Chapter 2. CNF Encodings; Chapter 3. Complete Algorithms; Chapter 4. CDCL Solvers; Chapter 5. Look-Ahead Based SAT Solvers; Chapter 6. Incomplete Algorithms; Chapter 7. Fundaments of Branching Heuristics; Chapter 8. Random Satisfiability; Chapter 9. Exploiting Runtime Variation in Complete Solvers; Chapter 10. Symmetry and Satisfiability; Chapter 11. Minimal Unsatisfiability and Autarkies; Chapter 12. Worst-Case Upper Bounds; Chapter 13. Fixed-Parameter Tractability
Part II. Applications and ExtensionsChapter 14. Bounded Model Checking; Chapter 15. Planning and SAT; Chapter 16. Software Verification; Chapter 17. Combinatorial Designs by SAT Solvers; Chapter 18. Connections to Statistical Physics; Chapter 19. MaxSAT; Chapter 20. Model Counting; Chapter 21. Non-Clausal SAT and ATPG; Chapter 22. Pseudo-Boolean and Cardinality Constraints; Chapter 23. QBF Theory; Chapter 24. QBFs reasoning; Chapter 25. SAT Techniques for Modal and Description Logics; Chapter 26. Satisfiability Modulo Theories; Chapter 27. Stochastic Boolean Satisfiability; Subject Index Cited Author IndexContributing Authors and Affiliations |
| Record Nr. | UNINA-9910822485403321 |
| Amsterdam, The Netherlands ; ; Washington, DC, : IOS Press, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
R-Calculus, IV : propositional logic / / Wei Li and Yuefei Sui
| R-Calculus, IV : propositional logic / / Wei Li and Yuefei Sui |
| Autore | Li Wei |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2023] |
| Descrizione fisica | 1 online resource (264 pages) |
| Disciplina | 810 |
| Collana | Perspectives in Formal Induction, Revision and Evolution |
| Soggetto topico | Propositional calculus |
| ISBN |
9789811986338
9789811986321 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- R-calculus for simplified propositional logics -- R-calculi for tableau/Gentzen deduction systems -- R-calculi RQ1Q2/RQ1Q2 -- R-calculi RQ1iQ2j/RQ1iQ2j -- R-Calculi: RY1Q1iY2Q2j/RY1Q1iY2Q2j -- R-calculi for supersequents -- R-calculi for propositional logic. |
| Record Nr. | UNINA-9910683352003321 |
|
Li Wei
|
||
| Singapore : , : Springer, , [2023] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
R-Calculus, IV : propositional logic / / Wei Li and Yuefei Sui
| R-Calculus, IV : propositional logic / / Wei Li and Yuefei Sui |
| Autore | Li Wei |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Singapore : , : Springer, , [2023] |
| Descrizione fisica | 1 online resource (264 pages) |
| Disciplina | 810 |
| Collana | Perspectives in Formal Induction, Revision and Evolution |
| Soggetto topico | Propositional calculus |
| ISBN |
9789811986338
9789811986321 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Introduction -- R-calculus for simplified propositional logics -- R-calculi for tableau/Gentzen deduction systems -- R-calculi RQ1Q2/RQ1Q2 -- R-calculi RQ1iQ2j/RQ1iQ2j -- R-Calculi: RY1Q1iY2Q2j/RY1Q1iY2Q2j -- R-calculi for supersequents -- R-calculi for propositional logic. |
| Record Nr. | UNISA-996546834003316 |
|
Li Wei
|
||
| Singapore : , : Springer, , [2023] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theory and applications of satisfiability testing : 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004 : revised selected papers / / Holger H. Hoos, David G. Mitchell (eds.)
| Theory and applications of satisfiability testing : 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004 : revised selected papers / / Holger H. Hoos, David G. Mitchell (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2005 |
| Descrizione fisica | 1 online resource (XIII, 393 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
HoosHolger H
MitchellDavid G., Ph. D. |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Propositional calculus
Algebra, Boolean Computer algorithms Decision making |
| ISBN | 3-540-31580-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables -- Mapping Problems with Finite-Domain Variables to Problems with Boolean Variables -- A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints -- An Algebraic Approach to the Complexity of Generalized Conjunctive Queries -- Incremental Compilation-to-SAT Procedures -- Resolve and Expand -- Looking Algebraically at Tractable Quantified Boolean Formulas -- Derandomization of Schuler’s Algorithm for SAT -- Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank -- QBF Reasoning on Real-World Instances -- Automatic Extraction of Functional Dependencies -- Algorithms for Satisfiability Using Independent Sets of Variables -- Aligning CNF- and Equivalence-Reasoning -- Using DPLL for Efficient OBDD Construction -- Approximation Algorithm for Random MAX-kSAT -- Clause Form Conversions for Boolean Circuits -- From Spin Glasses to Hard Satisfiable Formulas -- CirCUs: A Hybrid Satisfiability Solver -- Equivalence Models for Quantified Boolean Formulas -- Search vs. Symbolic Techniques in Satisfiability Solving -- Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems -- Satisfiability Threshold of the Skewed Random k-SAT -- NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances -- Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems -- UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT -- SAT Solver Competition and QBF Solver Evaluation (Invited Papers) -- Fifty-Five Solvers in Vancouver: The SAT 2004 Competition -- March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver -- Zchaff2004: An Efficient SAT Solver -- The Second QBF Solvers Comparative Evaluation. |
| Altri titoli varianti | SAT 2004 |
| Record Nr. | UNINA-9910484593503321 |
| Berlin, : Springer, 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theory and applications of satisfiability testing : 8th international conference, SAT 2005, St Andrews, UK, June 19-23, 2005 : proceedings / / Fahiem Bacchus, Toby Walsh (eds.)
| Theory and applications of satisfiability testing : 8th international conference, SAT 2005, St Andrews, UK, June 19-23, 2005 : proceedings / / Fahiem Bacchus, Toby Walsh (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2005 |
| Descrizione fisica | 1 online resource (XII, 492 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
BacchusFahiem
WalshToby |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Preface -- Solving Over-Constrained Problems with SAT Technology -- A Symbolic Search Based Approach for Quantified Boolean Formulas -- Substitutional Definition of Satisfiability in Classical Propositional Logic -- A Clause-Based Heuristic for SAT Solvers -- Effective Preprocessing in SAT Through Variable and Clause Elimination -- Resolution and Pebbling Games -- Local and Global Complete Solution Learning Methods for QBF -- Equivalence Checking of Circuits with Parameterized Specifications -- Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming -- Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution -- Resolution Tunnels for Improved SAT Solver Performance -- Diversification and Determinism in Local Search for Satisfiability -- On Finding All Minimally Unsatisfiable Subformulas -- Optimizations for Compiling Declarative Models into Boolean Formulas -- Random Walk with Continuously Smoothed Variable Weights -- Derandomization of PPSZ for Unique-k-SAT -- Heuristics for Fast Exact Model Counting -- A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic -- DPvis – A Tool to Visualize the Structure of SAT Instances -- Constraint Metrics for Local Search -- Input Distance and Lower Bounds for Propositional Resolution Proof Length -- Sums of Squares, Satisfiability and Maximum Satisfiability -- Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable -- A New Approach to Model Counting -- Benchmarking SAT Solvers for Bounded Model Checking -- Model-Equivalent Reductions -- Improved Exact Solvers for Weighted Max-SAT -- Quantifier Trees for QBFs -- Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas -- A Branching Heuristics for Quantified Renamable Horn Formulas -- An Improved Upper Bound for SAT -- Bounded Model Checking with QBF -- Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies -- Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas -- Automated Generation of Simplification Rules for SAT and MAXSAT -- Speedup Techniques Utilized in Modern SAT Solvers -- FPGA Logic Synthesis Using Quantified Boolean Satisfiability -- On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization -- A New Set of Algebraic Benchmark Problems for SAT Solvers -- A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas -- Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability -- On Subsumption Removal and On-the-Fly CNF Simplification. |
| Altri titoli varianti | SAT 2005 |
| Record Nr. | UNINA-9910483132503321 |
| Berlin ; ; New York, : Springer, 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
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 | ||
| ||
Theory and applications of satisfiability testing--SAT 2006 : 9th international conference, Seattle, WA, USA, August 12-15, 2006 : proceedings / / Armin Biere, Carla P. Gomes (eds.)
| Theory and applications of satisfiability testing--SAT 2006 : 9th international conference, Seattle, WA, USA, August 12-15, 2006 : proceedings / / Armin Biere, Carla P. Gomes (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2006 |
| Descrizione fisica | 1 online resource (XII, 440 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
BiereArmin
GomesCarla |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico |
Propositional calculus
Decision making Computer algorithms Algebra, Boolean |
| ISBN | 3-540-37207-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- From Propositional Satisfiability to Satisfiability Modulo Theories -- CSPs: Adding Structure to SAT -- Session 1. Proofs and Cores -- Complexity of Semialgebraic Proofs with Restricted Degree of Falsity -- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel -- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction -- Minimum Witnesses for Unsatisfiable 2CNFs -- Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs -- Extended Resolution Proofs for Symbolic SAT Solving with Quantification -- Session 2. Heuristics and Algorithms -- Encoding CNFs to Empower Component Analysis -- Satisfiability Checking of Non-clausal Formulas Using General Matings -- Determinization of Resolution by an Algorithm Operating on Complete Assignments -- A Complete Random Jump Strategy with Guiding Paths -- Session 3. Applications -- Applications of SAT Solvers to Cryptanalysis of Hash Functions -- Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies -- Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ -- SAT in Bioinformatics: Making the Case with Haplotype Inference -- Session 4. SMT -- Lemma Learning in SMT on Linear Constraints -- On SAT Modulo Theories and Optimization Problems -- Fast and Flexible Difference Constraint Propagation for DPLL(T) -- A Progressive Simplifier for Satisfiability Modulo Theories -- Session 5. Structure -- Dependency Quantified Horn Formulas: Models and Complexity -- On Linear CNF Formulas -- A Dichotomy Theorem for Typed Constraint Satisfaction Problems -- Session 6. MAX-SAT -- A Complete Calculus for Max-SAT -- On Solving the Partial MAX-SAT Problem -- MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in Time -- Average-Case Analysis for the MAX-2SAT Problem -- Session 7. Local Search and Survey Propagation -- Local Search for Unsatisfiability -- Efficiency of Local Search -- Implementing Survey Propagation on Graphics Processing Units -- Characterizing Propagation Methods for Boolean Satisfiability -- Session 8. QBF -- Minimal False Quantified Boolean Formulas -- Binary Clause Reasoning in QBF -- Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares -- QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency -- Session 9. Counting and Concurrency -- Solving #SAT Using Vertex Covers -- Counting Models in Integer Domains -- sharpSAT – Counting Models with Advanced Component Caching and Implicit BCP -- A Distribution Method for Solving SAT in Grids. |
| Altri titoli varianti | SAT 2006 |
| Record Nr. | UNINA-9910484504903321 |
| Berlin, : Springer, 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
