UnitWalk: A new SAT solver that uses local search guided by unit clause elimination

DOI10.1007/s10472-005-0421-9zbMath1100.68621OpenAlexW4253362517MaRDI QIDQ1777395

Arist Kojevnikov, Edward A. Hirsch

Publication date: 13 May 2005

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-005-0421-9

zbMATH Keywords

local searchempirical evaluationBoolean satisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Randomized algorithms (68W20)

Related Items (15)

A comparative runtime analysis of heuristic algorithms for satisfiability problems ⋮ The state of SAT ⋮ A Computing Procedure for Quantification Theory ⋮ The analysis of expected fitness and success ratio of two heuristic optimizations on two bimodal MaxSat problems ⋮ Combining incomplete search and clause generation: an application to the orienteering problems with time windows ⋮ A Decision-Making Procedure for Resolution-Based SAT-Solvers ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances ⋮ On SAT instance classes and a method for reliable performance experiments with SAT solvers ⋮ UnitWalk: A new SAT solver that uses local search guided by unit clause elimination ⋮ A SAT approach to query optimization in mediator systems ⋮ GridSAT: Design and implementation of a computational grid application ⋮ An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses ⋮ UnitWalk ⋮ A parallelization scheme based on work stealing for a class of SAT solvers

Uses Software

• SatEx
• SATLIB
• Walksat
• Chaff
• Velev SAT Benchmarks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A continuous approach to inductive inference
• Solving satisfiability in less than \(2^ n\) steps
• On the greedy algorithm for satisfiability
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Local search algorithms for SAT: an empirical evaluation
• UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
• A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search.
• SAT local search algorithms: Worst-case study
• Implementing the Davis-Putnam method
• Algorithms for Sat and upper bounds on their complexity
• An improved exponential-time algorithm for k -SAT
• GRASP: a search algorithm for propositional satisfiability
• Local search characteristics of incomplete SAT procedures

This page was built for publication: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination