SAT-Based Formula Simplification

DOI10.1007/978-3-319-24318-4_21zbMath1471.68245OpenAlexW2287661067MaRDI QIDQ3453233

Alexey Ignatiev, Alessandro Previti, João P. Marques-Silva

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_21

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)

Related Items (2)

Minimal sets on propositional formulae. Problems and reductions ⋮ Optimal symmetry breaking for graph problems

Uses Software

• MiniSat
• Glucose
• ABC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast, flexible MUS enumeration
• Quantified maximum satisfiability
• A note on the complexity of Boolean concepts
• A GRASP algorithm to solve the unicost set covering problem
• Complexity minimization in rule-based category learning: revising the catalog of Boolean concepts and evidence for non-minimal rules
• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A theory of diagnosis from first principles
• Efficient 2 and 3-flip neighborhood search algorithms for the MAX SAT: experimental Evaluation
• Iterative and core-guided maxsat solving: a survey and assessment
• Logic minimization techniques with applications to cryptology
• Redundancy in logic. I: CNF propositional formulae
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form
• Efficient Privacy-Preserving Ciphertext-Policy Attribute Based-Encryption and Broadcast Encryption
• Towards efficient MUS extraction
• A Way to Simplify Truth Functions
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Input Variable Assignment and Output Phase Optimization of PLA's
• Minimal Logic Programs
• Two-level logic minimization: an overview
• Theory and Applications of Satisfiability Testing
• Quantified Maximum Satisfiability:
• Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• The Problem of Simplifying Truth Functions

This page was built for publication: SAT-Based Formula Simplification