MaxSAT resolution for regular propositional logic

DOI10.1016/j.ijar.2023.109010MaRDI QIDQ6066845

Jordi Coll, Chu-Min Li, Elifnaz Yangin, Felip Manyà

Publication date: 16 November 2023

Published in: International Journal of Approximate Reasoning (Search for Journal in Brave)

zbMATH Keywords

resolutionvariable eliminationmaximum satisfiabilitymultiple-valued logicsigned CNF formulasregular CNF formulas

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Many-valued logic (03B50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Boolean lexicographic optimization: algorithms \& applications
• Compiling finite linear CSP into SAT
• Resolution for Max-SAT
• The intractability of resolution
• On tackling the limits of resolution in SAT solving
• A tableau calculus for non-clausal maximum satisfiability
• Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
• A logical approach to efficient Max-SAT solving
• Resolution procedures for multiple-valued optimization
• Equivalence between systems stronger than resolution
• Towards a better understanding of (partial weighted) MaxSAT proof systems
• Mapping CSP into Many-Valued SAT
• Exploiting Cycle Structures in Max-SAT
• Short Conjunctive Normal Forms in Finitely Valued Logics
• ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver
• New Tableau Characterizations for Non-clausal <scp>MaxSAT</scp> Problem
• Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem
• Solving the Team Composition Problem in a Classroom
• Theory and Applications of Satisfiability Testing

This page was built for publication: MaxSAT resolution for regular propositional logic