scientific article; zbMATH DE number 956865

zbMath0868.03007MaRDI QIDQ5687274

Yumi K. Tsuji, Allen van Gelder

Publication date: 19 August 1997

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

reasoningguessingstatistical performance analysisDavis-Putnam algorithm\(k\)-limited resolutionalgorithm for propositional satisfiabilityapplication of statistics to computer experiments

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)

Related Items

Semantically-guided goal-sensitive reasoning: model representation ⋮ Propositional SAT Solving ⋮ Partitioning methods for satisfiability testing on large formulas ⋮ Unnamed Item ⋮ Approximating minimal unsatisfiable subformulae by means of adaptive core search ⋮ Equivalent literal propagation in the DLL procedure ⋮ On the limit of branching rules for hard random unsatisfiable 3-SAT ⋮ New methods for 3-SAT decision and worst-case analysis ⋮ Another look at graph coloring via propositional satisfiability ⋮ Efficient data structures for backtrack search SAT solvers ⋮ Toward leaner binary-clause reasoning in a satisfiability solver ⋮ A complete adaptive algorithm for propositional satisfiability ⋮ How good are branching rules in DPLL? ⋮ Solving satisfiability problems using elliptic approximations -- effective branching rules ⋮ Partitioning methods for satisfiability testing on large formulas ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ A parallelization scheme based on work stealing for a class of SAT solvers

Uses Software

• PSATO