Complete Boolean satisfiability solving algorithms based on local search

DOI10.1007/S11390-013-1326-4zbMATH Open1280.68241OpenAlexW2094668451MaRDI QIDQ2434568FDOQ2434568

Authors Wensheng Guo, William N. N. Hung, Xiaoyu Song, Guowu Yang 

Publication date 6 February 2014

Published in Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11390-013-1326-4

zbMATH Keywords

setlocal searchcliqueBoolean satisfiabilitycomplete search

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• scientific article; zbMATH DE number 2084740
• scientific article; zbMATH DE number 5575002
• scientific article; zbMATH DE number 2090309
• scientific article; zbMATH DE number 1903342
• Selection of search strategies for solving 3-SAT problems

Cites Work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 5547826 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• scientific article; zbMATH DE number 1448978 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A note on treewidth in random graphs
• Adaptive channel and power allocation of downlink multi-user MC-CDMA systems
• Cross-layer packet scheduling for downlink multiuser OFDM systems
• Local search with edge weighting and configuration checking heuristics for minimum vertex cover
• Many hard examples in exact phase transitions
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Random constraint satisfaction: easy generation of hard (satisfiable) instances
• SATzilla: portfolio-based algorithm selection for SAT
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Two Hardness Results on Feedback Vertex Sets

Cited In (8)

• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Zeon and idem-Clifford formulations of Boolean satisfiability
• Title not available (Why is no real title available?)
• Selection of search strategies for solving 3-SAT problems
• Propagation based local search for bit-precise reasoning

Uses Software

• zChaff
• SATzilla
• RSat

This page was built for publication: Complete Boolean satisfiability solving algorithms based on local search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2434568)