Pages that link to "Item:Q5613969"

The following pages link to A Computing Procedure for Quantification Theory (Q5613969):

Displaying 50 items.

• MaxMinMax problem and sparse equations over finite fields (Q285259) (← links)
• Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
• Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
• Stochastic enumeration method for counting NP-hard problems (Q352890) (← links)
• Simulating circuit-level simplifications on CNF (Q352967) (← links)
• Satisfiability of acyclic and almost acyclic CNF formulas (Q385062) (← links)
• On Davis-Putnam reductions for minimally unsatisfiable clause-sets (Q391124) (← links)
• Towards NP-P via proof complexity and search (Q408544) (← links)
• Exact algorithms for dominating set (Q411862) (← links)
• Finding kernels or solving SAT (Q414435) (← links)
• Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models (Q415616) (← links)
• Toward a model for backtracking and dynamic programming (Q430838) (← links)
• A note on SAT algorithms and proof complexity (Q436581) (← links)
• On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
• An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
• Dealing with satisfiability and \(n\)-ary CSPs in a logical framework (Q438582) (← links)
• Incremental preprocessing methods for use in BMC (Q453488) (← links)
• Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search (Q457253) (← links)
• Curriculum-based course timetabling with SAT and MaxSAT (Q475170) (← links)
• Quantifier elimination by dependency sequents (Q479823) (← links)
• An overview of parallel SAT solving (Q487635) (← links)
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability (Q502391) (← links)
• Prominent classes of the most general subsumptive solutions of Boolean equations (Q507645) (← links)
• Dealing with 4-variables by resolution: an improved MaxSAT algorithm (Q515546) (← links)
• Efficient branch-and-bound algorithms for weighted MAX-2-SAT (Q535012) (← links)
• John McCarthy's legacy (Q543573) (← links)
• Leveraging belief propagation, backtrack search, and statistics for model counting (Q545553) (← links)
• Algorithms for four variants of the exact satisfiability problem (Q596105) (← links)
• A weight-balanced branching rule for SAT (Q597527) (← links)
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
• A characteristic set method for solving Boolean equations and applications in cryptanalysis of stream ciphers (Q611072) (← links)
• Projecting systems of linear inequalities with binary variables (Q646699) (← links)
• Matroid enumeration for incidence geometry (Q664549) (← links)
• Meta-resolution: An algorithmic formalisation (Q671650) (← links)
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
• A continuous approach to inductive inference (Q687090) (← links)
• Linearity and regularity with negation normal form (Q703486) (← links)
• Engineering constraint solvers for automatic analysis of probabilistic hybrid automata (Q710668) (← links)
• Foundations of \(r\)-contiguous matching in negative selection for anomaly detection (Q734206) (← links)
• Short propositional refutations for dense random 3CNF formulas (Q741088) (← links)
• Efficient generation of small interpolants in CNF (Q746773) (← links)
• A dual algorithm for the satisfiability problem (Q750165) (← links)
• Negation in rule-based database languages: A survey (Q753476) (← links)
• Negation by default and unstratifiable logic programs (Q753501) (← links)
• Algorithms for the maximum satisfiability problem (Q753502) (← links)
• Computational experience with an interior point algorithm on the satisfiability problem (Q753688) (← links)
• Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT (Q764375) (← links)
• Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models (Q785238) (← links)
• Unrestricted vs restricted cut in a tableau method for Boolean circuits (Q812394) (← links)
• A parallelization scheme based on work stealing for a class of SAT solvers (Q812442) (← links)