Name
Abstract | ||
|---|---|---|
Minimum Satisfiability (MinSAT) denotes one of the optimization versions of the Boolean Satisfiability (SAT) problem. In some settings MinSAT is preferred to using Maximum Satis-fiability (MaxSAT). Several encodings and dedicated branch and bound algorithms for MinSAT have been recently proposed, and evaluated on small challenging randomly generated instances. Motivated by the observation that current best performing MaxSAT algorithms for structured and industrial instances are based on computing unsatisfiable cores with a SAT solver, this paper proposes novel approaches for MinSAT, that also target these instances. First, the paper proposes an algorithm based on iteratively calling a SAT solver which uses the computed models to relax clauses. Second, the paper proposes group-based MinSAT solving, which is essentially a novel reduction of the MinSAT problem into the Group MaxSAT problem. For a given MinSAT instance, the resulting Group MaxSAT formula is then translated into a standard MaxSAT formula which specifically targets unsatisfiability-based MaxSAT algorithms. Experimental results indicate that, similarly to MaxSAT, the proposed approaches outperform branch and bound algorithms on problem instances obtained from practical applications. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/ICTAI.2012.129 | ICTAI), 2012 IEEE 24th International Conference |
Keywords | Field | DocType |
Boolean functions,computability,group theory,iterative methods,optimisation,branch and bound algorithms,group-based MinSAT solving,iterative SAT solving,maximum satisfiability,minimum satisfiability,optimized Boolean satisfiability problem,randomly generated instances,relax clauses,unsatisfiability-based group MaxSAT algorithms,unsatisfiable core computing,Boolean Optimization,Maximum Satisfiability,Minimum Satisfiability | Boolean function,Maximum satisfiability problem,Branch and bound,Iterative method,Computer science,Satisfiability,Boolean satisfiability problem,Algorithm,Computability,Benchmark (computing) | Conference |
Volume | ISSN | ISBN |
1 | 1082-3409 | 978-1-4799-0227-9 |
Citations | PageRank | References |
8 | 0.45 | 15 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Federico Hers | 1 | 8 | 0.45 |
| Antonio Morgado | 2 | 8 | 0.45 |
| Jordi Planes | 3 | 486 | 31.38 |
| Joao Marques-Silva | 4 | 8 | 0.45 |