scientific article; zbMATH DE number 1113992

Jun Gu, Paul Walton jun. Purdom, John V. Franco, Benjamin W.-S. Wah

Publication date: 2 March 1998

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

survey performance evaluation satisfiability problem practical applications SAT algorithms algorithm space

Analysis of algorithms and problem complexity (68Q25) Applications of mathematical programming (90C90) Combinatorial optimization (90C27) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42) Classical propositional logic (03B05) Algorithms in computer science (68W99)

Related Items (47)

Nagging: A scalable fault-tolerant paradigm for distributed search ⋮ Improving a fixed parameter tractability time bound for the shadow problem ⋮ An Improved SAT Algorithm in Terms of Formula Length ⋮ Understanding the role of noise in stochastic local search: analysis and experiments ⋮ Improved MaxSAT Algorithms for Instances of Degree 3 ⋮ Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances ⋮ A weight-balanced branching rule for SAT ⋮ Analysis and solving SAT and MAX-SAT problems using an \(L\)-partition approach ⋮ An Experimental Evaluation of Fast Approximation Algorithms for the Maximum Satisfiability Problem ⋮ Resolution and linear CNF formulas: improved \((n,3)\)-\textsc{MaxSAT} algorithms ⋮ Differentiable learning of matricized DNFs and its application to Boolean networks ⋮ The set of parameterized \(k\)-covers problem ⋮ Bounded Synthesis ⋮ Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks ⋮ Worst-case study of local search for MAX-\(k\)-SAT. ⋮ A satisfiability procedure for quantified Boolean formulae ⋮ Toward a model for backtracking and dynamic programming ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ New methods for 3-SAT decision and worst-case analysis ⋮ Satisfiability in composition-nominative logics ⋮ Reactive local search techniques for the maximum \(k\)-conjunctive constraint satisfaction problem \((MAX-k-CCSP)\) ⋮ The \(Multi\)-SAT algorithm ⋮ Elliptic approximations of propositional formulae ⋮ Experimental complexity analysis of continuous constraint satisfaction problems. ⋮ A logic-based approach to polymer sequence analysis ⋮ Solving peptide sequencing as satisfiability ⋮ Controlled generation of hard and easy Bayesian networks: Impact on maximal clique size in tree clustering ⋮ ANALYSIS AND SOLUTION OF DISCRETE OPTIMIZATION PROBLEMS WITH LOGICAL CONSTRAINTS ON THE BASE OF L-PARTITION APPROACH ⋮ ANALYSIS OF L-STRUCTURE OF POLYHEDRON IN THE PARTIAL MAX SAT PROBLEM ⋮ Dealing with 4-variables by resolution: an improved MaxSAT algorithm ⋮ An improved semidefinite programming relaxation for the satisfiability problem ⋮ A cost-reducing question-selection algorithm for propositional knowledge-based systems ⋮ On SAT instance classes and a method for reliable performance experiments with SAT solvers ⋮ On exact selection of minimally unsatisfiable subformulae ⋮ UnitWalk: A new SAT solver that uses local search guided by unit clause elimination ⋮ Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT ⋮ Logical and algorithmic properties of stable conditional independence ⋮ New tractable classes for default reasoning from conditional knowledge bases ⋮ Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem ⋮ Efficient Monte Carlo simulation via the generalized splitting method ⋮ Evaluating ASP and commercial solvers on the CSPLib ⋮ Unnamed Item ⋮ Accelerating branch-and-bound through a modeling language construct for relaxation-specific constraints ⋮ Backtracking tactics in the backtrack method for SAT ⋮ Formal verification of a generic framework to synthesize SAT-provers ⋮ Unrestricted vs restricted cut in a tableau method for Boolean circuits ⋮ The Service-Oriented Multiagent Approach to High-Performance Scientific Computing

Uses Software

This page was built for publication: