Decomposing SAT Instances with Pseudo Backbones

DOI10.1007/978-3-319-55453-2_6MaRDI QIDQ3304190zbMATH OpenOpenAlexFDO

Authors Wen-Xiang Chen, Darrell Whitley

Publication date 5 August 2020

Published in Evolutionary Computation in Combinatorial Optimization (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-55453-2_6

zbMATH Keywords

decompositionpartition crossoverpseudo-backbonesatisfiabilitytreewidthvisualization

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Approximation methods and heuristics in mathematical programming (90C59)

Recommendations

• An expressive model for instance decomposition based parallel SAT solvers
• Decomposing SAT problems into connected components
• Backdoors into heterogeneous classes of SAT and CSP
• Solving satisfiability using decomposition and the most constrained subproblem
• scientific article; zbMATH DE number 5139168
• scientific article; zbMATH DE number 5139161
• Computing optimal hypertree decompositions with SAT
• Solving d-SAT via Backdoors to Small Treewidth

Cites work

• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Bounded model checking using satisfiability solving
• Combining Adaptive Noise and Look-Ahead in Local Search for SAT
• Complexity of Finding Embeddings in a k-Tree
• Computer Solutions of the Traveling Salesman Problem
• Computer-aided proof of Erdős discrepancy properties
• Configuration landscape analysis and backbone guided local search. I: Satisfiability and maximum satisfiability
• Determining computational complexity from characteristic ``phase transitions
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Graph minors. II. Algorithmic aspects of tree-width
• scientific article; zbMATH DE number 4060712 (Why is no real title available?)
• Partition Crossover for Pseudo-Boolean Optimization
• Partition-based logical reasoning for first-order and propositional theories
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Using Community Structure to Detect Relevant Learnt Clauses
• Visualizing SAT instances and runs of the DPLL algorithm

Cited in

(5)

• Blocked clause decomposition
• Decomposing SAT problems into connected components
• Towards backbone computing: a greedy-whitening based approach
• Partition Crossover can Linearize Local Optima Lattices of k-bounded Pseudo-Boolean Functions
• Reduction-based MAX-3SAT with low nonlinearity and lattices under recombination

Describes a project that uses

Uses Software

• MiniSat
• UBCSAT
• BG-WalkSAT
• Velev SAT Benchmarks

This page was built for publication: Decomposing SAT Instances with Pseudo Backbones

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