Visualizing SAT instances and runs of the DPLL algorithm

DOI10.1007/s10817-007-9074-1zbMath1129.68502OpenAlexW2010166520MaRDI QIDQ2462641

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)

Related Items (2)

Recognition of Nested Gates in CNF Formulas ⋮ Decomposing SAT Instances with Pseudo Backbones

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Algorithms for drawing graphs: An annotated bibliography
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Ordered semantic hyper-linking
• Fixed-parameter complexity in AI and nonmonotonic reasoning
• Directed hypergraphs and applications
• Partitioning methods for satisfiability testing on large formulas
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• Proving consistency assertions for automotive product data management
• Resolution versus search: Two strategies for SAT
• Bucket elimination: A unifying framework for reasoning
• BerkMin: A fast and robust SAT-solver
• Formula Caching in DPLL
• Graph-Based Algorithms for Boolean Function Manipulation
• Graph minors. II. Algorithmic aspects of tree-width
• Complexity of Finding Embeddings in a k-Tree
• A Multilevel Algorithm for Force-Directed Graph-Drawing
• Scalable error detection using boolean satisfiability
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Collective dynamics of ‘small-world’ networks
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies
• Principles and Practice of Constraint Programming – CP 2004
• Computer Aided Verification
• A fast algorithm for particle simulations
• Bounded model checking using satisfiability solving

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