scientific article; zbMATH DE number 3313427
From MaRDI portal
zbMath0197.00102MaRDI QIDQ5593816
Publication date: 1968
Full work available at URL: https://eudml.org/doc/188127
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
On finding short resolution refutations and small unsatisfiable subsets, On the complexity of resolution with bounded conjunctions, On an MCS-based inconsistency measure, Propositional SAT Solving, SAT-Based Model Checking, Resolution vs. cutting plane solution of inference problems: Some computational experience, Temporal Answer Set Programming on Finite Traces, A satisfiability tester for non-clausal propositional calculus, Local and global symmetry breaking in itemset mining, Optimizing propositional calculus formulas with regard to questions of deducibility, Formal methods for reasoning and uncertainty reduction in evidential grid maps, Minimal sets on propositional formulae. Problems and reductions, Short resolution proofs for a sequence of tricky formulas, Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms, Temporal Equilibrium Logic with past operators, Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving, Verification Modulo theories, Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems, Thirty years of Epistemic Specifications, Extended clause learning, Generalized probabilistic satisfiability and applications to modelling attackers with side-channel capabilities, Resolution and binary decision diagrams cannot simulate each other polynomially, Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets, Equivalent literal propagation in the DLL procedure, Unnamed Item, A pearl on SAT and SMT solving in Prolog, Efficient computation of answer sets via SAT modulo acyclicity and vertex elimination, Abstract interpretation of microcontroller code: intervals meet congruences, New methods for 3-SAT decision and worst-case analysis, The \(Multi\)-SAT algorithm, On a generalization of extended resolution, Recognition of tractable satisfiability problems through balanced polynomial representations, Disjunctive closures for knowledge compilation, Semidefinite resolution and exactness of semidefinite relaxations for satisfiability, An Introduction to Lower Bounds on Resolution Proof Systems, Tractability of cut-free Gentzen type propositional calculus with permutation inference, Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs, Propositional proof systems based on maximum satisfiability, Finding Effective SAT Partitionings Via Black-Box Optimization, Generalized probabilistic satisfiability, Mining top-\(k\) motifs with a SAT-based framework, Resolution over linear equations and multilinear proofs, Intra- and interdiagram consistency checking of behavioral multiview models, Counting truth assignments of formulas of bounded tree-width or clique-width, Using Abduction to Compute Efficient Proofs, Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity, Asymptotic cyclic expansion and bridge groups of formal proofs, Extension without cut, On propositional coding techniques for the distinguishability of objects in finite sets, Several notes on the power of Gomory-Chvátal cuts, Cycling in proofs and feasibility, On the complexity of cutting-plane proofs, Efficient suspect selection in unreachable state diagnosis, Resolution with counting: dag-like lower bounds and different moduli, Reversible pebble games and the relation between tree-like and general resolution space, plasp 3: Towards Effective ASP Planning, The complexity of error metrics, On tseitin formulas, read-once branching programs and treewidth, Unnamed Item, Definability for model counting, Propositional proof complexity, Finding a tree structure in a resolution proof is NP-complete, Turning cycles into spirals, Average time analyses of simplified Davis-Putnam procedures, Resolution over linear equations modulo two, Expansion-based QBF solving versus Q-resolution, Bigraphs with sharing, Streams and strings in formal proofs., Space bounds for resolution, Bounded Model Checking with Parametric Data Structures, Interpolant Learning and Reuse in SAT-Based Model Checking, Compressing BMC Encodings with QBF, GhostQ, On average time hierarchies, Study of discrete automaton models of gene networks of nonregular structure using symbolic calculations, Learning Optimal Decision Sets and Lists with SAT, On the query complexity of selecting minimal sets for monotone predicates, Reflections on Proof Complexity and Counting Principles, Davis and Putnam meet Henkin: solving DQBF with resolution, Hardness and optimality in QBF proof systems modulo NP, Characterizing Tseitin-formulas with short regular resolution refutations
