scientific article; zbMATH DE number 3325539
From MaRDI portal
Publication:5604434
zbMath0205.00402MaRDI QIDQ5604434
Publication date: 1968
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ Automated generation of exam sheets for automated deduction ⋮ A lower bound for tree resolution ⋮ Diverse Palindromic Factorization Is NP-complete ⋮ Empirical analysis of algorithms for the shortest negative cost cycle problem ⋮ Verifying the conversion into CNF in dafny ⋮ An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs ⋮ Lower Bounds for the Size of Nondeterministic Circuits ⋮ On black-box optimization in divide-and-conquer SAT solving ⋮ Craig interpolation with clausal first-order tableaux ⋮ The power of the binary value principle ⋮ Computer-aided proof of Erdős discrepancy properties ⋮ Regular and General Resolution: An Improved Separation ⋮ Towards NP-P via proof complexity and search ⋮ Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas ⋮ Boolean functional synthesis: from under the hood of solvers ⋮ Learning Boolean specifications ⋮ A comparison of ASP-based and SAT-based algorithms for the contension inconsistency measure ⋮ A logical encoding for \(k\)-\(m\)-realization of extensions in abstract argumentation ⋮ Gregory Samuilovich Tseytin (obituary) ⋮ Simulating strong practical proof systems with extended resolution ⋮ Mass Customization and “Forecasting Options’ Penetration Rates Problem” ⋮ Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases ⋮ The NP-hardness of finding a directed acyclic graph for regular resolution ⋮ On the complexity of choosing the branching literal in DPLL ⋮ Diverse Palindromic Factorization is NP-Complete ⋮ Conflict-driven answer set solving: from theory to practice ⋮ Feasibly constructive proofs of succinct weak circuit lower bounds ⋮ A new 3-CNF transformation by parallel-serial graphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem ⋮ Strong extension-free proof systems ⋮ Non-clausal redundancy properties ⋮ Boolean satisfiability in quantum compilation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Investigations on autark assignments ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ On the restricted equivalence for subclasses of propositional logic ⋮ A Recursive Inclusion Checker for Recursively Defined Subtypes ⋮ Solving QBF with counterexample guided refinement ⋮ A Logical Autobiography ⋮ DiMo -- discrete modelling using propositional logic
