PicoSAT

swMATH7092MaRDI QIDQ19150

No author found.

Related Items (85)

Two disjoint 5-holes in point sets ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Prolog Technology Reinforcement Learning Prover ⋮ Formalization and implementation of modern SAT solvers ⋮ 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 ⋮ Expressing Symmetry Breaking in DRAT Proofs ⋮ SATenstein: automatically building local search SAT solvers from components ⋮ Cobra: A Tool for Solving General Deductive Games ⋮ Compositional Propositional Proofs ⋮ Unnamed Item ⋮ Parallel MUS Extraction ⋮ Mechanical Verification of SAT Refutations with Extended Resolution ⋮ Taming high treewidth with abstraction, nested dynamic programming, and database technology ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ On tackling the limits of resolution in SAT solving ⋮ Incremental bounded model checking for embedded software ⋮ Strategyproof social choice when preferences and outcomes may contain ties ⋮ Formalization of Abstract State Transition Systems for SAT ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Adaptive Restart Strategies for Conflict Driven SAT Solvers ⋮ Solving projected model counting by utilizing treewidth and its limits ⋮ SAT-solving in CSP trace refinement ⋮ Automatically comparing memory consistency models ⋮ Rewriting logic and its applications. 8th international workshop, WRLA 2010, held as a satellite event of ETAPS 2010, Paphos, Cyprus, March 20--21, 2010. Revised selected papers ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Curriculum-based course timetabling with SAT and MaxSAT ⋮ Quantifier elimination by dependency sequents ⋮ SAT-Solving Based on Boundary Point Elimination ⋮ Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories ⋮ 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 ⋮ On Some Multicolor Ramsey Numbers Involving $K_3+e$ and $K_4-e$ ⋮ SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata ⋮ 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 ⋮ Decision procedures. An algorithmic point of view ⋮ Practical algorithms for unsatisfiability proof and core generation in SAT solvers ⋮ Producing and verifying extremely large propositional refutations ⋮ Automatic Evaluation of Context-Free Grammars (System Description) ⋮ 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 ⋮ Testing and debugging techniques for answer set solver development ⋮ Automated Testing and Debugging of SAT and QBF Solvers ⋮ Exact DFA Identification Using SAT Solvers ⋮ Improving Unsatisfiability-Based Algorithms for Boolean Optimization ⋮ Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT ⋮ Two Techniques for Minimizing Resolution Proofs ⋮ Minimising Deterministic Büchi Automata Precisely Using SAT Solving ⋮ Assignment Stack Shrinking ⋮ Rewriting, Inference, and Proof ⋮ Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games ⋮ Unnamed Item ⋮ Unnamed Item ⋮ 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 ⋮ Boundary Points and Resolution ⋮ Solving (Weighted) Partial MaxSAT through Satisfiability Testing ⋮ Algorithms for Weighted Boolean Optimization ⋮ Unnamed Item ⋮ Gardens of Eden in the game of life ⋮ SAT-Based Preprocessing for MaxSAT ⋮ Iterative and core-guided maxsat solving: a survey and assessment ⋮ Implementing Efficient All Solutions SAT Solvers ⋮ On Computing Backbones of Propositional Theories ⋮ 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

This page was built for software: PicoSAT