腅....3
1. ......4
2. 셅....8
2.1 WalkSAT...9
2.2 GSAT14
.15
.............16
. , , . , .
( SAT) , , . . , .
: ().
, , : CSP (Constraint Satisfaction Problem) ( , ). , , ( ).
NP-, . , .
, (SAT-) 1000 . , ( : industrial) . ( , ) . , (3SAT-) 700.
, . ,
DPLL-. :
- , .
- , .
, ( ), , (automated theorem proving) (circuit verification).
|
|
|
(Davis) (Putnam) 1960 .. : . , (Logemann) (Loveland) 1962 . . DLL DPLL, DP. . , , DPLL-.
, DPLL, :
- Conflict-driven (minisat, vallst, zChaff).
- Look-ahead (kcnfs, march, OKsolver).
, , , 3-. Conict-driven- . Look-ahead- . , , .
DPLL
1. - (BCP).
2. , .
3. ,
.
4. , (
).
5. , .
6. x ( , ).
7. DPLL (x).
8. DPLL (! x).
9. ,
.
10. .
:
public static class DPLL
{
public static bool Solve(Expression e)
{
if (IsSat(e))
{
return true;
}
if (ContainEmptyDisunkt(e))
return false;
List<List<ILiteral>> oneLitDis = OneLitDis(e);
foreach (var dis in oneLitDis)
{
e = UnitPropagade(e, dis);
}
Literal l = ChooseLiteral(e);
if (l == null)
{
return IsSat(e);
}
return Solve(e.Add(l)) || Solve(e.Add(Not(l)));
}
:
(x V y) ^ z, (a) ^ (!a), .
:
T(n)
| N | DPLL | ||
| 0,002 | |||
| 0,000667 | |||
| 0,0156 | |||
| 0,0052 | |||
| 1,48 | 1,43 | 1,41 | |
| 1,44 | |||
| 31,54 | 31,43 | 31,46 | |
| 31,48 | |||
| 116,132 | 115,84 | 115,68 | |
| 115,88 | |||
| >1800 | >1800 | >1800 | |
T(max) = 1800, N=30.
.
,
. , (local search) . , , . , ( ) . , (: , ). (). . . .
|
|
|
GSAT , (Stochastic Local Search),
.
WalkSAT , 1997 . GSAT . WalkSAT , . , ().
(, ,
).
.
. .
, , . : , , ..
, SAT. , MAXSAT ( , ). , ( ).
WalkSAT
:
public static bool Solve(Expression e, int MaxTries,int MaxFlips)
{
for (int i = 0; i < MaxTries; i++)
{
SetRandomValues(e);
for (int flip = 0; flip < MaxFlips; flip++)
{
List<Literal> c = RandomUnsatClause(e);
Literal l = GetRandomLiteral(c);
if (l!= null)
{
Flip(l);
}
if (IsSat(e))
return true;
}
}
return false;
}
MaxTries , MaxFlips .
:
(x V y) ^ z, (a) ^ (!a), .
:
T(n).
| T() | ||||||
| N | DPLL | WalkSAT | ||||
| 0,002 | 0,002 | |||||
| 0,000667 | 0,000667 | |||||
| 0,0156 | 0,0156 | |||||
| 0,0052 | 0,0052 | |||||
| 1,48 | 1,43 | 1,41 | 0,046 | |||
| 1,44 | 0,0156 | |||||
| 31,54 | 31,43 | 31,46 | 0,08 | |||
| 31,48 | 0,026 | |||||
| 116,132 | 115,84 | 115,68 | 0,06 | 0,047 | 0,036 | |
| 115,88 | 0,048 | |||||
| >1800 | >1800 | >1800 | 0,42 | 0,36 | 0,6 | |
| 0,46 | ||||||
| 0,97 | 0,8 | 0,96 | ||||
| 0,91 | ||||||
| 4,95 | 4,97 | 4,93 | ||||
| 4,95 | ||||||
| >1800 | ||||||
T(max) = 1800, max = 1000.
.
| T() | ||||||||
| N | DPLL | WalkSAT | DPLL | WalkSAT | ||||
| 0,002 | 0,002 | True | True | |||||
| 0,000667 | 0,000667 | |||||||
| 0,0156 | 0,0156 | True | True | |||||
| 0,0052 | 0,0052 | |||||||
| 1,48 | 1,43 | 1,41 | 0,046 | True | True | |||
| 1,44 | 0,0156 | |||||||
| 31,54 | 31,43 | 31,46 | 0,08 | True | True | |||
| 31,48 | 0,026 | |||||||
| 116,132 | 115,84 | 115,68 | 0,06 | 0,047 | 0,036 | True | False | |
| 115,88 | 0,048 | |||||||
| >1800 | >1800 | >1800 | 0,42 | 0,36 | 0,6 | True | False | |
| 0,46 | ||||||||
| 0,97 | 0,8 | 0,96 | False | |||||
| 0,91 | ||||||||
| 4,95 | 4,97 | 4,93 | False | |||||
| 4,95 | ||||||||
| False | ||||||||
| >1800 | False | |||||||
|
|
|
, DPLL . WalkSAT , n4.
N
ε=100l(St - Sp)l/St
N
ε=100l(Tt - Tp)l/Tt
| 98,91667 | |
| 99,91741 | |
| 99,95858 | |
| 99,97444 |
.
GSAT
. . , . , , . , GSAT. , , . , (, 10).
:
public static class GSat
{
public static bool Solve(Expression e, int MaxTries, int MaxFlips)
{
for (int i = 0; i < MaxTries; i++)
{
SetRandomValues(e);
for (int flip = 0; flip < MaxFlips; flip++)
{
List<Literal> c = RandomUnsatClause(e);
Literal l = GetLiteralGreedily(e, c);
if (l!= null)
{
Flip(l);
}
if (IsSat(e))
return true;
}
}
return false;
}
private static void Flip(Literal l)
{
l.Value =!l.Value;
}
private static List<Literal> RandomUnsatClause(Expression e)
{
List<List<Literal>> clauses = new List<List<Literal>>();
foreach (var clause in e.Clauses)
{
bool temp = false;
foreach (var lit in clause)
{
temp = temp || (lit.Not)?!lit.Value.Value: lit.Value.Value;
}
if (!temp)
clauses.Add(clause);
}
if (clauses.Count > 0)
return clauses[(new Random()).Next(clauses.Count)];
else
return null;
}
private static void SetRandomValues(Expression e)
{
Random r = new Random();
foreach (var l in e.Literals)
{
if (e.Literals.Where(lit => lit.Name == l.Name).Count() == 1)
l.Value = r.NextDouble() > 0.5;
else
{
bool value = r.NextDouble() > 0.5;
foreach (var literal in e.Literals.Where(lit => lit.Name == l.Name))
{
literal.Value = value;
}
}
}
}
private static Literal GetLiteralGreedily(Expression e, List<Literal> clause)
{
Dictionary<int, Literal> raitingLiteral = new Dictionary<int, Literal>();
foreach (var literal in clause)
{
int currentNumberUnsatClauses = CountUnsatClauses(e);
Flip(literal);
int flippedNumber = CountUnsatClauses(e);
if (flippedNumber < currentNumberUnsatClauses)
try
{
raitingLiteral.Add(currentNumberUnsatClauses - flippedNumber, literal);
}
catch { }
Flip(literal);
}
if (raitingLiteral.Count > 0)
{
int maxScore = raitingLiteral.Keys.Max();
|
|
|
return raitingLiteral[maxScore];
}
return null;
}
private static int CountUnsatClauses(Expression e)
{
List<List<Literal>> clauses = new List<List<Literal>>();
foreach (var clause in e.Clauses)
{
bool temp = false;
foreach (var lit in clause)
{
temp = temp || (lit.Not)?!lit.Value.Value: lit.Value.Value;
}
if (!temp)
clauses.Add(clause);
}
return clauses.Count;
}
private static bool IsSat(Expression e)
{
List<bool> temp = new List<bool>();
temp.Add(true);
foreach (var list in e.Clauses)
{
foreach (Literal l in e.Literals)
{
if (l.Value == null)
return false;
}
bool result = list[0].Not?!list[0].Value.Value: list[0].Value.Value;
for (int i = 1; i < list.Count; i++)
{
bool intermed = list[i].Not?!list[i].Value.Value: list[i].Value.Value;
result = result || intermed;
}
temp.Add(result);
}
bool res = temp[0];
for (int i = 1; i < temp.Count; i++)
res = res && temp[i];
return res;
}
}
:
() ^ (a), (a) ^ (!a), .
:
T(n).
| T(n) | ||||||
| N | DPLL | GSAT | ||||
| 190010,6667 | 156675,3333 | |||||
| 170009,6667 | ||||||
| 486691,3333 | ||||||
| 1336860,333 | ||||||
| 316371,6667 | ||||||
| 8627163,667 | ||||||
| 773503,3333 | ||||||
| 1246732,333 | ||||||
| 2056784,333 |
T(max) = 2056784,333, max = 1000.
.
| T(n) | ||||||||
| N | DPLL | GSAT | DPLL | GSAT | ||||
| True | True | |||||||
| 190010,6667 | 156675,3333 | |||||||
| True | True | |||||||
| 170009,6667 | ||||||||
| False | True | |||||||
| 486691,3333 | ||||||||
| False | True | |||||||
| 1336860,333 | ||||||||
| False | True | |||||||
| 316371,6667 | ||||||||
| False | True | |||||||
| 8627163,667 | ||||||||
| False | True | |||||||
| False | True | |||||||
| 773503,3333 | ||||||||
| False | True | |||||||
| 1246732,333 | ||||||||
| False | True | |||||||
| 2056784,333 |
, DPLL . GSAT , n3.
N
ε=100l(St - Sp)l/St
