PaperlayerView exact revision on arXiv

Source-linked AI summary

New Inference Rules for Max-SAT

C. M. Li, F. Manya, J. Planes

arXiv:1111.0040v1cs.AI

TL;DR

Exact Max-SAT solvers cannot freely use SAT unit propagation because it may change the number of unsatisfied clauses. The paper introduces equivalent-preserving inference rules, proves their soundness through an integer-programming transformation, and evaluates them in MaxSatz, which is reported as competitive across several instance families and benchmarks.

  • Problem

    SAT-style unit propagation and existing lower-bound methods do not directly provide equivalent Max-SAT simplifications and can repeatedly rediscover contradictions.

  • Method

    The paper defines sound Max-SAT inference rules, proves them via an integer-programming transformation, and incorporates them into the MaxSatz solver.

  • Results

    MaxSatz is reported as very competitive on random Max-2SAT, random Max-3SAT, Max-Cut, Graph 3-coloring, and Max-SAT Evaluation 2006 instances.

  • Takeaways & Limitations

    The inference rules make lower-bound computation more incremental and improve lower-bound quality, while exposing contradictions so they need not be repeatedly detected.

  • Takeaways & Limitations

    The effectiveness of rule applications depends on unit-clause propagation order, and further study is needed to find orderings that maximize their use.

Abstract

from arXiv · show

Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

1. Introduction

The paper addresses the gap between SAT and exact Max-SAT solvers by adapting SAT-style inference while preserving Max-SAT equivalence. It introduces sound inference rules, implements them in MaxSatz, and reports competitive performance across several instance families and benchmarks.

  • Exact Max-SAT solvers use less inference than SAT solvers because ordinary unit propagation preserves satisfiability but not Max-SAT equivalence.For some assignments, the original and propagated formulas have different numbers of unsatisfied clauses.
  • Existing lower-bound methods detect inconsistencies but may repeatedly rediscover them without making unsatisfied clauses explicit.Good lower bounds prune search, yet lower-bound computation alone does not simplify the formula.
  • The paper defines sound inference rules that transform a Max-SAT instance into an equivalent, easier-to-solve instance.In Max-SAT, soundness means preserving the number of unsatisfied clauses for every complete assignment.
  • The rules expose contradictions and can increase the lower bound by 2 instead of 1 while avoiding repeated detection below the current node.The added clause may enable another contradiction to be detected through unit propagation.
  • The rules form a Max-SAT counterpart of SAT unit propagation, combining previously known rules with rules original to Max-SAT.They were selected for natural and efficient application.
  • MaxSatz incorporates the inference rules and a previous lower bound, and is reported as very competitive on random Max-2SAT, random Max-3SAT, Max-Cut, Graph 3-coloring, and Max-SAT Evaluation 2006 instances.The paper evaluates the practical power of the inference rules through this solver.

2. Preliminaries

The preliminaries define propositional variables, literals, clauses, CNF formulas, assignments, and Max-SAT. They also specify the equivalence relation used for Max-SAT formulas.

  • A propositional variable takes value 0 or 1, a literal is a variable or its negation, and a clause is a disjunction of literals.A CNF formula is a conjunction of clauses, and its size sums the lengths of its clauses.
  • An assignment satisfies a clause when it satisfies at least one literal, while an empty clause cannot be satisfied.A complete assignment assigns all variables occurring in the formula.
  • Max-SAT finds an assignment minimizing unsatisfied clauses, equivalently maximizing satisfied clauses.MaxkSAT restricts every clause to k literals, and formulas are represented as clause multisets.
  • Two CNF formulas are equivalent when every complete assignment gives them the same number of unsatisfied clauses.

3. A Basic Max-SAT Solver

The basic solver uses depth-first branch and bound with lower bounds from current violations plus underestimation, pruning branches that cannot improve the incumbent. Its underestimation procedure repeatedly detects disjoint inconsistent subsets using unit propagation.

  • The branch-and-bound solver explores the assignment search tree depth-first and compares an upper bound with a lower bound at each node.The lower bound combines currently empty clauses with an underestimation of future violations.
  • If the lower bound reaches or exceeds the upper bound, the solver prunes the current subtree and backtracks.The upper bound is the number of unsatisfied clauses in the best complete assignment found so far.
  • When the lower bound remains below the upper bound, the solver branches on a selected variable, creating false and true child branches.
  • The solver's result is the final upper-bound value after the entire search tree has been explored.
  • The underestimation procedure repeatedly applies unit propagation, removes clauses used to derive an empty clause, and counts detected inconsistent subsets.It stops when no empty clause is derived or when the lower bound reaches the upper bound.
  • For the example formula, unit propagation detects three disjoint inconsistent subsets, giving an underestimation of 3.The three detections are listed as successive reductions of the remaining formula.

4. Inference Rules

The paper defines sound Max-SAT inference rules that preserve equivalence while making contradictions explicit and potentially strengthening lower bounds. Their soundness follows from an integer-programming transformation, and the rules include both established and original refinements of unit resolution.

  • Inference rules: The rules are selected as efficient refinements of unit resolution and transform equivalent Max-SAT instances into easier-to-solve instances.Some rules were known from prior work, while others are original to Max-SAT.
  • Soundness: An integer-programming transformation represents each clause’s unsatisfied status and proves equivalence when two formulas have equal objective values for every complete assignment.The transformation extends to empty clauses, which contribute one to the objective.
  • Basic rules: Rules 1 and 2 cover shortened resolution and complementary unit clauses, with Rule 2 replacing complementary units by an empty clause.The replacement preserves equivalence and lets the contradiction contribute directly to lower bounds without being redetected.
  • Rules 3 and 4: Rule 3 and Rule 4 make contradictions explicit while adding clauses that can improve lower bounds through later inference or inconsistent subsets.Rule 3 replaces three clauses with an empty clause and an added binary clause; Rule 4 captures a linear unit-resolution refutation.
  • Rules 3 and 4: Rules 3 and 4 consume two unit clauses per contradiction, potentially preventing those clauses from detecting two later disjoint conflicts.The paper identifies this trade-off for empirical analysis.
  • Rules 5 and 6: Rules 5 and 6 capture refutations consuming exactly one unit clause, while adding clauses and preserving further conflict detection through unit propagation.These rules make contradictions explicit, support more incremental lower-bound computation, and do not limit detection of further conflicts via unit propagation.

5. Implementation of Inference Rules

The implementation detects Max-SAT inference-rule applicability through unit-propagation implication graphs, transforms formulas while increasing lower bounds, and terminates with linear space complexity. The implementation is sound but not necessarily complete because propagation order can prevent applicable rules from being applied.

  • Rule implementation: Inference rules remove clauses, insert new clauses, and increase the lower bound by 1 while reducing formula size.The transformed formula contains fewer literals and clauses, and new clauses can reuse storage for old ones.
  • Rule applicability: Rules 3–6 detect contradictions by analyzing paths to complementary literals in the implication graph.The associated clauses form inconsistent subsets, and Lemmas 2 and 3 characterize chain structures that enable the rules.
  • Implication graph: Unit propagation constructs an acyclic implication graph whose nodes are literals and whose edges encode clause-based implications.The graph contains one node for each distinct literal reached, with duplicate unit clauses represented by a single node.
  • Rules 3 and 4: Rules 3 and 4 rewrite binary clauses in an inconsistent subset, remove its unit clauses, and increment the empty-clause count.Their applicability requires unit-rooted implication chains ending in complementary literals.
  • Rules 5 and 6: Rules 5 and 6 apply when the contradiction structure contains an implication chain plus exactly three nodes outside the chain.The proof identifies the corresponding clause pattern and shows how the rule conditions arise.
  • Complexity and completeness: The implementation uses linear space and always terminates, but propagation order can leave applicable inference rules undiscovered.The rules are sound, yet the implementation is not necessarily complete; further study of propagation order is suggested.
  • Extensions: The inference rules can be naturally extended to weighted Max-SAT, where clauses carry weights and unsatisfied-clause weights are minimized.The paper gives a weighted analogue of Rule 3 as an example.

6. MaxSatz: a New Max-SAT Solver

MaxSatz is a new solver combining unit-propagation lower bounds with six inference rules and additional simplification and branching techniques. The paper compares it with simplified solver variants that apply different subsets of the rules.

  • Solver design: MaxSatz incorporates unit-propagation lower bounds and applies Rules 1 through 6.It also includes techniques inherited from SAT solving and several Max-SAT-specific heuristics.
  • Additional techniques: MaxSatz additionally uses pure-literal, Empty-Unit clause, Dominating Unit Clause, variable-selection, and value-selection techniques.The variable and value heuristics weight binary clauses four times more than other clauses.
  • Solver variants: The experimental comparison uses MaxSat0, MaxSat12, and MaxSat1234 as simplified versions of MaxSatz.These variants differ in whether they apply the defined inference rules.
  • Solver variants: MaxSat12 applies Rules 1 and 2, whereas MaxSat1234 additionally applies Rules 3 and 4.MaxSat12 uses a special unit-propagation ordering with two queues, Q1 and Q2.
  • Implementation: Source code for MaxSat0, MaxSat12, MaxSat1234, and MaxSatz is made available at two listed URLs.The implementations support direct reproduction of the solver comparisons.

7. Experimental Results

Experiments evaluated the inference rules and compared MaxSatz with other Max-SAT solvers across random, structured, and benchmark instances. MaxSatz consistently improved solving performance, with gains attributed to stronger lower bounds, smaller search trees, and incremental conflict handling.

  • Inference-rule evaluation: For 50-variable and 100-variable Max-2SAT, MaxSatz was 7.6 and 9.2 times faster than MaxSat1234 at 1000 clauses, respectively.The gains increased with the number of variables and clauses, and MaxSatz also produced substantially smaller search trees.
  • Inference-rule evaluation: For Max-3SAT, MaxSat1234 was 36% faster at 600 clauses and 44% faster at 1000 clauses for 70-variable instances, while Rules 5 and 6 improved MaxSatz's lower bound and runtime.The runtime gain increased as the number of clauses increased.
  • Inference-rule evaluation: For Max-Cut with 800 edges, MaxSatz's search tree was 40 times smaller and its runtime was 47 times faster than MaxSat1234.Rules 5 and 6 were more powerful than Rules 3 and 4 on these structured binary-clause instances.
  • Inference-rule evaluation: On graph 3-coloring, Rules 1 and 2 were not useful, whereas the other rules reduced search-tree size by deriving better lower bounds.The instances used 24 and 60 vertices with edge densities from 20% to 90%.
  • Comparison with other solvers: Across external comparisons, MaxSatz was up to two orders of magnitude faster on hard random Max-2SAT instances and was best performing on Max-Cut, graph 3-coloring, and all Max-SAT Evaluation 2006 sets.For one random Max-2SAT comparison, MaxSatz solved an instance in 1 second while MaxSolver and toolbar exceeded 10,000 seconds; it also solved three MAXCUT johnson instances within the time limit versus two for other solvers.

8. Related Work

Related work covers lower-bound methods based on inconsistency detection, arc consistency, and inference rules, while highlighting MaxSatz’s unit-propagation-guided approach. Earlier soft arc-consistency methods require variable orderings, whereas the proposed rules do not.

  • Lower-bound computation: Lower-bound methods range from inconsistency counts and DAC counts to star rules and unit propagation for detecting contradictions.UP subsumes inconsistent-count and star-rule methods, while DAC-based methods address binary clauses.
  • Consistency transformations: Projection and extension are equivalence-preserving transformations that connect soft local consistency techniques with Max-SAT inference rules.Projection replaces complementary binary clauses with a unit clause, while extension reverses that operation.
  • Consistency transformations: Unguided extension can undo previous projections, so directional arc consistency uses variable orderings to guide transformations.Choosing an ordering that efficiently exploits soft arc consistency remains an open problem.
  • The proposed approach: MaxSatz’s inference-rule approach avoids predefined variable orderings because unit propagation guides combinations of projection and extension operations.The approach extends projection and extension to constraints involving more than two variables through higher-order rules.
  • Weighted Max-SAT: Related work independently introduced chain and cycle resolution rules for weighted Max-SAT, extending the paper’s resolution rules.Future work proposed implementing cycle resolution to evaluate detection overhead and compare it with MaxSatz.

9. Conclusions and Future Work

The paper addresses weak contradiction detection and repeated lower-bound computation in exact Max-SAT by introducing efficient, equivalence-preserving inference rules. Experiments with MaxSatz found the approach competitive across several instance families, while future work targets rule ordering, new ternary rules, and weighted Max-SAT.

  • Conclusions: Existing Max-SAT solvers repeatedly recompute contradictions and use conservative lower bounds, motivating inference rules that simplify equivalent instances.The rules are based on contradictions detected by unit propagation and are intended especially for hard instances containing many contradictions.
  • Conclusions: MaxSatz incorporates the inference rules, and experiments found empirical improvements in lower-bound incrementality and quality compared with MaxSatz without them.The solver was also reported faster than other compared solvers, with gains of several orders of magnitude on the hardest instances.
  • Conclusions: Across the reported benchmark families, MaxSatz was more robust than other solvers because different competitors performed best on different problem types.The cited second-best solvers varied across Max-2SAT, Max-3SAT, Max-Cut, and graph 3-coloring.
  • Future work: Future work will study unit-clause ordering, develop ternary-clause inference rules, and extend the results to weighted Max-SAT.The weighted setting is linked to applications including maximum clique, set covering, combinatorial auctions, and constraint satisfaction.
Loading 1111.0040v1…