Solving Satisfiability with Less Searching

DOI10.1109/TPAMI.1984.4767555MaRDI QIDQ3335000zbMATH OpenWikidataFDO

Authors Paul Walton jun. Purdom

Publication date 1984

Published in IEEE Transactions on Pattern Analysis and Machine Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/TPAMI.1984.4767555

zbMATH Keywords

constraint satisfactionsatisfiabilitysubtreesSearch treesDavis-Putnam procedurecomplement searchingconjunctive normal form predicatespure literals

Mathematics Subject Classification ID

Searching and sorting (68P10)

Recommendations

• Solving propositional satisfiability problems
• scientific article; zbMATH DE number 956858
• A Computational Study of Satisfiability Algorithms for Propositional Logic
• Theory and Applications of Satisfiability Testing
• scientific article; zbMATH DE number 1008453

Cited in

(23)

• New methods for 3-SAT decision and worst-case analysis
• On a generalization of extended resolution
• Polynomial-average-time satisfiability problems
• Solving satisfiability problems with preferences
• New methods for proving the impossibility to solve problems through reduction of problem spaces
• Optimizing with minimum satisfiability
• Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences
• Theory and Applications of Satisfiability Testing
• Solving the incremental satisfiability problem
• Searching with iterated maps
• A logical framework for depiction and image interpretation
• scientific article; zbMATH DE number 5575002 (Why is no real title available?)
• An efficient algorithm for the 3-satisfiability problem
• Solving propositional satisfiability problems
• An artificial neural network satisfiability tester
• scientific article; zbMATH DE number 4049072 (Why is no real title available?)
• scientific article; zbMATH DE number 2084724 (Why is no real title available?)
• Simulating circuit-level simplifications on CNF
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability
• Ordered model trees: A normal form for disjunctive deductive databases
• CHAMP: a multipass algorithm for Max Sat based on saver variables
• Solving satisfiability using decomposition and the most constrained subproblem
• Present and Future of Practical SAT Solving

This page was built for publication: Solving Satisfiability with Less Searching

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