Visualizing SAT instances and runs of the DPLL algorithm

DOI10.1007/S10817-007-9074-1MaRDI QIDQ2462641zbMATH OpenOpenAlexFDO

Authors Carsten Sinz

Publication date 3 December 2007

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

Full work available at URL https://doi.org/10.1007/s10817-007-9074-1

zbMATH Keywords

DPLL procedureSAT instance

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Theory and Applications of Satisfiability Testing
• \textsf{SATGraf}: visualizing the evolution of SAT formula structure in solvers
• scientific article; zbMATH DE number 956858
• scientific article; zbMATH DE number 5605058
• Locality and hard SAT-instances

Cites work

• A Computing Procedure for Quantification Theory
• A fast algorithm for particle simulations
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A Multilevel Algorithm for Force-Directed Graph-Drawing
• Algorithms for drawing graphs: An annotated bibliography
• BerkMin: A fast and robust SAT-solver
• Bounded model checking using satisfiability solving
• Bucket elimination: A unifying framework for reasoning
• Collective dynamics of `small-world' networks
• Complexity of Finding Embeddings in a k-Tree
• Computer Aided Verification
• Decomposing SAT problems into connected components
• Directed hypergraphs and applications
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Fixed-parameter complexity in AI and nonmonotonic reasoning
• Formula Caching in DPLL
• Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies
• Graph minors. II. Algorithmic aspects of tree-width
• Graph-Based Algorithms for Boolean Function Manipulation
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• scientific article; zbMATH DE number 5139160 (Why is no real title available?)
• scientific article; zbMATH DE number 5139164 (Why is no real title available?)
• scientific article; zbMATH DE number 67483 (Why is no real title available?)
• scientific article; zbMATH DE number 1956604 (Why is no real title available?)
• scientific article; zbMATH DE number 1467488 (Why is no real title available?)
• scientific article; zbMATH DE number 1369843 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Ordered semantic hyper-linking
• Partitioning methods for satisfiability testing on large formulas
• Principles and Practice of Constraint Programming – CP 2004
• Proving consistency assertions for automotive product data management
• Resolution versus search: Two strategies for SAT
• Scalable error detection using Boolean satisfiability
• 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
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(4)

• Decomposing SAT Instances with Pseudo Backbones
• \textsf{SATGraf}: visualizing the evolution of SAT formula structure in solvers
• Recognition of Nested Gates in CNF Formulas
• Theory and Applications of Satisfiability Testing

Describes a project that uses

Uses Software

• Velev SAT Benchmarks
• MiniSat
• DPvis
• Chaff
• BerkMin

This page was built for publication: Visualizing SAT instances and runs of the DPLL algorithm

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