scientific article; zbMATH DE number 6970793
From MaRDI portal
Publication:4553279
DOI10.23638/LMCS-14(4:3)2018zbMath1403.68239arXiv1702.05527MaRDI QIDQ4553279
Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
Publication date: 2 November 2018
Full work available at URL: https://arxiv.org/abs/1702.05527
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Solving QBF with counterexample guided refinement
- Simulating circuit-level simplifications on CNF
- Super-Blocked Clauses
- Blocked Clause Decomposition
- Inprocessing Rules
- Clause Elimination for SAT and QSAT
- Efficient CNF Simplification Based on Binary Implication Graphs
- Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- A Unified Proof System for QBF Preprocessing
- Recognition of Nested Gates in CNF Formulas
- Playing with AVATAR
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
- Using SAT in QBF
- Blocked Clause Elimination
- Verifying Refutations with Extended Resolution
- Soundness of Inprocessing in Clause Sharing SAT Solvers
- Concurrent Clause Strengthening
- A Computing Procedure for Quantification Theory
- Theory and Applications of Satisfiability Testing
This page was built for publication:
