Phokion G. Kolaitis Thomas RaffillComputer Science DepartmentUC Santa Cruz
Phase Transitions A phase transition is an abrupt change in the behavior of a property of a “system”.Extensive study of phase transitions in physics (statistical mechanics).Extensive study of phase transitions in NP-complete problems during the past decade.
Understand the “structure” of NP-complete problems.Relate phase transitions to the average-case performance of particular algorithms for NP-complete problems.
NP-Complete Problems Introduce a “constrainedness” parameter to partition the space of instances.Generate random instances at fixed parameter values.For some problems, probability of a “yes” instance abruptly changes from 1 to 0 at some critical value.For some problems and some solvers, average difficulty peaks sharply at the same critical value.
Main Example: 3-SAT Parameter: Ratio of number of clauses to number of variables.Intuition: Low ratios are underconstrained, high ratios are overconstrained.Critical Value: Experimental results suggest that it is about 4.3 clauses to variables. Average Performance: DPLL procedure peaks around 4.3
AC-Matching Term matching under an operation that is associative & commutative (no unit). a1X1+ … + anXn = AC b1C1+ …+ bmCmExample: 2X1+X2 = AC 4C1+ 5C2- Solution 1: X1 2C1 , X2 5C2
- Solution 2: X1 C1 , X2 2 C1+ 5C2
- Solution 3: X1 2C1+C2 , X2 3C2
- Solution 4: …
-
AC-Matching AC-matching plays an important role in automated deduction.AC-matching solvers are key components of many theorem-provers (eg., EQP). (it is NP-complete even if the coefficients are given in unary).
Parametrization of AC-Matching Several different parameters come into play: number of variables, number of constants, maximum coefficients, … a1X1+ … + anXn = AC b1C1+ …+ bmCmOur chosen parameter: r = ( ai ) / ( bj) Some intuition:- more variables more constrained instance
- more constants less constrained instance
- reflects both # of symbols and multiplicities.
NP-Completeness for Fixed Ratios Definition: AC(r)-Matching is the restriction of AC-Matching to instances of ratio r.Fact: If r > 1, then every instance of AC(r)-Matching is negative.Theorem: If r is such that 0 < r 1, then AC(r)-Matching is NP-complete. -- r = 1: 3-Partition is reducible to AC(1)-Matching (Eker – 1993). -- 0 < r < 1: By careful padding, can reduce AC(1)-Matching to AC(r)-Matching.
Pr(r,s) = probability that a random instance of AC(r)-Matching of size s is positive, where s = ai + bj .Conjecture: There is critical ratio r* s.t.- If r < r*, then Pr(r,s) 1 , as s ;
- If r > r*, then Pr(r,s) 0 , as s .
Generating Random Instances Fix size s.Step through ratios u/v 1, where u+v = s.Generate random partitions of u and v.Use the partition of u for LHS coefficients; Use the partition of v for RHS coefficients.1200 samples give < 4% margin of error with 95% confidence.30000 samples give < 1% margin of error.
Solvers Used in Experiments Direct AC-Matching Solver developed by S. Eker at SRI as part of Maude, a high-performance system for equational logic and rewriting.Reduction to Integer Linear Programming (ILP) and CPLEX, a commercial optimization package with a powerful ILP solver.Reduction to SAT and Grasp, one of the main SAT solvers developed by J. Silva.
Given an instance of AC-Matching a1X1+ … + anXn = AC b1C1+ …+ bmCm express each Xi as a non-empty linear combination of the Cjs: Xi ijCjResulting instance of ILP is: iaiij = bj , 1 j m jij 1 , 1 i n.Standard reduction of ILP to SAT.
Prob. of solvability as function of r based on 1200 samples
Large-Scale Experiments Initial experiments based on instances of size up to 400 and on samples of size 1200 suggest a possible crossover near ratio 42:58Large-scale experiments were carried out on the interval of ratios [30:70, 50:50]- Instance sizes: 100, 200, 400, 800, 1600
- Sample size: 30000 random instances for each data point.
Large-Scale Experiments: Close-up on Critical Region
Finite-Size Scaling Given a family of curves f(r,s) for various instance sizes s, rescale x-axis according to a power law r = [(r – r*)/r*] sSuperimpose curves f(r,s) by replacing each data point (r,p) by the point ( [(r – r*)/r*] s , p).Check whether the curves f(r,s) collapse to a universal function f(r) which is monotone and takes values between 1 and 0 as r varies from - to .The existence of a universal function supports phase transition conjecture: in the vicinity of r*, the values of f(r,s) jump from 1 to 0 as s .
Results of Finite-Size Scaling: Probability Curves Collapse
Validation of Finite-Size Scaling
Slowly Emerging Phase Transition? Curve-fitting gives the power law r' = [(r 0.73)/0.73] s 0.171 critical ratio r* = 0.73 42:58 scaling exponent = 0.171Scaling exponent is rather small (scaling exponent for 3-SAT is in [0.625, 0.714]) .This suggests that any phase transition for AC-matching emerges very slowly.
Extrapolation to Very Large Sizes
The three solvers were run on the instance sets and CPU time was recorded.Maude and Reduction to ILP + CPLEX are fast on almost all instances.Reduction to SAT + Grasp is much slower than either Maude or Reduction to ILP + CPLEX.Reduction to SAT + Grasp has sharp peak in solving time near the critical ratio 0.73
Median Time of Reduction to SAT + Grasp
70th percentile of Reduction to SAT + Grasp
Concluding Remarks There is some evidence for a phase transition in AC-Matching based on experimental results and finite-size scaling.However, in contrast to 3-SAT and several other NP-complete problems, the phase-transition in AC-Matching emerges very slowly.Limitation of experimental methods: analytical results are needed to provide more convincing evidence or demonstrate its existence.
Concluding Remarks Maude and CPLEX-based solver show no change in performance near the critical ratio. Will this change with larger-size instances?Grasp-based solver peaks near the critical ratio. Will this change with a better reduction of AC-matching to SAT and/or a different SAT solver?
Do'stlaringiz bilan baham: |
