Publication:3604000

From MaRDI portal


zbMath1159.68403MaRDI QIDQ3604000

Armin Biere

Publication date: 24 February 2009



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

68P05: Data structures


Related Items

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores, On L-shaped point set embeddings of trees: first non-embeddable examples, Prolog Technology Reinforcement Learning Prover, Implementing Efficient All Solutions SAT Solvers, Proofs and Certificates for Max-SAT, PicoSAT, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Checking EMTLK properties of timed interpreted systems via bounded model checking, On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\), SAT-solving in CSP trace refinement, Algorithms for computing minimal equivalent subformulas, Curriculum-based course timetabling with SAT and MaxSAT, Quantifier elimination by dependency sequents, An overview of parallel SAT solving, Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Producing and verifying extremely large propositional refutations, On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, Two disjoint 5-holes in point sets, Minimal sets on propositional formulae. Problems and reductions, Incremental bounded model checking for embedded software, On L-shaped point set embeddings of trees: first non-embeddable examples, Co-clustering under the maximum norm, 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, Gardens of Eden in the game of life, 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, Eliminating models during model elimination, Model checking and strategy synthesis for multi-agent systems for resource allocation, Faradžev Read-type enumeration of non-isomorphic CC systems, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games, Faster, higher, stronger: E 2.3, Iterative and core-guided maxsat solving: a survey and assessment, A unified framework for DPLL(T) + certificates, SATenstein: automatically building local search SAT solvers from components, Strategyproof social choice when preferences and outcomes may contain ties, Solving projected model counting by utilizing treewidth and its limits, 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, 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, Propositional SAT Solving, Evaluating CDCL Variable Scoring Schemes, Adaptive Restart Strategies for Conflict Driven SAT Solvers, Local Restarts, Boundary Points and Resolution, Solving (Weighted) Partial MaxSAT through Satisfiability Testing, Algorithms for Weighted Boolean Optimization


Uses Software