Solving satisfiability problems with preferences

DOI10.1007/s10601-010-9095-yzbMath1208.68199OpenAlexW2051475155MaRDI QIDQ606909

Enrico Giunchiglia, Emanuele Di Rosa, Marco Maratea

Publication date: 19 November 2010

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-010-9095-y

zbMATH Keywords

posetpreferencespropositional satisfiabilitySATDavis-Logemann-Loveland procedureliterals

Mathematics Subject Classification ID

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

Related Items

Implementing Preferences with asprin, Progress in clasp Series 3, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, SAT-Based Horn Least Upper Bounds, Cautious reasoning in ASP via minimal models and unsatisfiable cores, A max-term counting based knowledge inconsistency checking strategy and inconsistency measure calculation of fuzzy knowledge based systems, Minimal sets on propositional formulae. Problems and reductions, A general framework for preferences in answer set programming, ASP and subset minimality: enumeration, cautious reasoning and MUSes, Abstract Solvers for Computing Cautious Consequences of ASP programs, Boolean lexicographic optimization: algorithms \& applications, Enumeration of minimal models and MUSes in WASP, Analysis of cyclic fault propagation via ASP, Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases, A complexity perspective on entailment of parameterized linear constraints, Minimal intervention strategies in logical signaling networks with ASP, Abstraction-Based Algorithm for 2QBF, Paracoherent answer set computation, On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes, Mining top-\(k\) motifs with a SAT-based framework, Manipulation of Articulated Objects Using Dual-arm Robots via Answer Set Programming, MCS Extraction with Sublinear Oracle Queries, Iterative and core-guided maxsat solving: a survey and assessment, Solving QBF with counterexample guided refinement

Uses Software

• MiniSat
• Pueblo
• CP-nets
• MaxSolver
• PBS
• Chaff
• MiniMaxSat

Cites Work

• A linear-time transformation of linear inequalities into conjunctive normal form
• Unrestricted vs restricted cut in a tableau method for Boolean circuits
• Deterministic planning in the fifth international planning competition: PDDL3 and experimental evaluation of the planners
• A structure-preserving clause form translation
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• Prioritized logic programming and its application to commonsense reasoning
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Preferred answer sets for ordered logic programs
• optsat: A Tool for Solving SAT Related Optimization Problems
• Algorithms for Weighted Boolean Optimization
• Tools and Algorithms for the Construction and Analysis of Systems
• Logic Programming
• Theory and Applications of Satisfiability Testing
• Logic programming with satisfiability
• The complexity of resolution refinements
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2003
• Principles and Practice of Constraint Programming – CP 2003
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item