Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings

DOI10.1007/S10817-005-9011-0MaRDI QIDQ862408zbMATH OpenOpenAlexFDO

Authors Alan M. Frisch, Timothy J. Peugniez, Anthony J. Doggett, Peter W. Nightingale

Publication date 24 January 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-005-9011-0

zbMATH Keywords

search spaces

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Searching and sorting (68P10) Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 1149437
• scientific article; zbMATH DE number 956858
• SAT local search algorithms: Worst-case study
• Local search algorithms for SAT: an empirical evaluation
• Non-systematic search and no-good learning

Cites work

• scientific article; zbMATH DE number 1341458 (Why is no real title available?)
• scientific article; zbMATH DE number 1149437 (Why is no real title available?)
• scientific article; zbMATH DE number 1405442 (Why is no real title available?)
• A machine program for theorem-proving
• Balance and filtering in structured satisfiable problems. (Preliminary report)
• Control abstractions for local search
• Embedding partial Steiner triple systems is NP-complete
• Integer optimization by local search. A domain-independent approach
• Theory and Applications of Satisfiability Testing

Cited in

(10)

• scientific article; zbMATH DE number 1149437 (Why is no real title available?)
• Speeding up the constraint-based method in difference logic
• Theory and Applications of Satisfiability Testing
• Programming for modular reconfigurable robots
• Comparing Two Stochastic Local Search Algorithms for Constraint Satisfaction Problems
• A first polynomial non-clausal class in many-valued logic
• Propagation complete encodings of smooth DNNF theories
• Automatic generation of redundant models for permutation constraint satisfaction problems
• scientific article; zbMATH DE number 1822444 (Why is no real title available?)
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF

Describes a project that uses

Uses Software

• WSAT(OIP)
• Walksat
• CSPLib

This page was built for publication: Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings

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