scientific article

Publication date: 24 February 2009

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

SAT solver restarts occurrence lists proof traces watched literals

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

Related Items

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Two disjoint 5-holes in point sets ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Prolog Technology Reinforcement Learning Prover ⋮ A unified framework for DPLL(T) + certificates ⋮ Evaluating CDCL Variable Scoring Schemes ⋮ Propositional SAT Solving ⋮ Eliminating models during model elimination ⋮ Checking EMTLK properties of timed interpreted systems via bounded model checking ⋮ SATenstein: automatically building local search SAT solvers from components ⋮ Model checking and strategy synthesis for multi-agent systems for resource allocation ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Incremental bounded model checking for embedded software ⋮ Strategyproof social choice when preferences and outcomes may contain ties ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Adaptive Restart Strategies for Conflict Driven SAT Solvers ⋮ Local Restarts ⋮ Solving projected model counting by utilizing treewidth and its limits ⋮ SAT-solving in CSP trace refinement ⋮ Algorithms for computing minimal equivalent subformulas ⋮ On L-shaped point set embeddings of trees: first non-embeddable examples ⋮ Curriculum-based course timetabling with SAT and MaxSAT ⋮ Quantifier elimination by dependency sequents ⋮ Faradžev Read-type enumeration of non-isomorphic CC systems ⋮ An overview of parallel SAT solving ⋮ Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories ⋮ Co-clustering under the maximum norm ⋮ Minimally Unsatisfiable Boolean Circuits ⋮ On Improving MUS Extraction Algorithms ⋮ Failed Literal Detection for QBF ⋮ Captain Jack: New Variable Selection Heuristics in Local Search for SAT ⋮ Generalized Conflict-Clause Strengthening for Satisfiability Solvers ⋮ Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Producing and verifying extremely large propositional refutations ⋮ Conflict-driven answer set solving: from theory to practice ⋮ Synthesis of quantifier-free DNF sentences from inconsistent samples of strings with EF games and SAT ⋮ FSM inference from long traces ⋮ Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games ⋮ Internal Guidance for Satallax ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Incremental Determinization ⋮ Non-prenex QBF Solving Using Abstraction ⋮ Q-Resolution with Generalized Axioms ⋮ HordeQBF: A Modular and Massively Parallel QBF Solver ⋮ Faster, higher, stronger: E 2.3 ⋮ PicoSAT ⋮ Boundary Points and Resolution ⋮ Solving (Weighted) Partial MaxSAT through Satisfiability Testing ⋮ Algorithms for Weighted Boolean Optimization ⋮ Gardens of Eden in the game of life ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ On L-shaped point set embeddings of trees: first non-embeddable examples ⋮ Iterative and core-guided maxsat solving: a survey and assessment ⋮ Implementing Efficient All Solutions SAT Solvers ⋮ Proofs and Certificates for Max-SAT ⋮ OptiLog: a framework for SAT-based systems ⋮ On dedicated CDCL strategies for PB solvers ⋮ A proof builder for Max-SAT ⋮ DQBDD: an efficient BDD-based DQBF solver

Uses Software