Transcript 20081014012746

Extracting
Minimum Unsatisfiable Cores
with a Greedy Genetic Algorithm
Jianmin Zhang, Sikun Li, and Shengyu Shen
School of Computer Science, National University of Defense Technology
Australasian Joint Conference on
Artificial Intelligence AI 06
Abstract
Problem:
finding minimum unsatisfiable core
Method:
Efficient greedy genetic algorithm
takes advantage of the relationship between maximal
satisfiability and minimum unsatisfiability
generate all minimal UCs then select the smallest one
experiment:
SAT benchmarks from Automotive Product
Configuration
(size of 22 instances from 4k~8k clauses and 1.6k ~1.9k
variables)
compared with the branch-and-bound algorithm
Conclusion :
Efficient than branch-and-bound algorithm
Introduction
Explaining the causes of unsatisfiability of Boolean
formulas is a key requirement in formal verification,
artificial intelligence, and electronic design.
p
checking minimal unsatisfiability is hard ? D complete
a smallest sub-formula that is also unsatisfiable
(minimum unsatisfiable core).
How to find minimun unsat core ?
Using relationship between maximal satisfiability and
minimal unsatisfiability
derive the complements of maximal satisfiable subsets.
extract a minimum unsatisfiable core by computing
the minimum hitting set of those complement sets
Related Work
Bruni and A. Sassano. Restoring Satisfiability or
Maintaining Unsatisfiability by Finding Small
Unsatisfiable Subformulae (SAT’01)
a method of adaptive core search
L. Zhang and S. Malik. Extracting small unsatisfiable
cores from unsatisfiable Boolean formula (SAT’03)
use SAT solvers to produce resolution refutations .
AMUSE: a minimally-unsatisfiable subformula
extractor.(DAC 04)
MUP: A minimal unsatisfiability prover.(DAC 05)
 : small unsatisfiable subformula no guarantee
minimal subformula
Related Work (con’t)
I. Lynce and J. P. Marques-Silva. On computing
minimum unsatisfiable cores.(SAT’04)
algorithm enumerates all possible subsets of a formula
and checks which are unsatisfiable
A branch and bound algorithm for extracting
smallest minimal unsatisfiable formulas. (SAT’05)
utilizes iterative maximal satisfiability solutions to
generate lower and upper bounds on smallest minimal UC
branch on specific subformulas to find it
 beter than previous
our approach compared with this on the same
benchmarks
Preliminaries
Definition 1. (Unsatisfiable Core).
Given a formula ϕ, ψ is an unsatisfiable core for ϕ iff ψ is
an unsatisfiable formula and ψ ⊆ ϕ.
Definition 2. (Minimal Unsatisfiable Core).
Given an unsatisfiable core ψ for a formula ϕ, ψ is a
minimal unsatisfiable core iff removing any clause ω∈ ψ
from ψ implies that ψ − {ω} is satisfiable.
Definition 3. (Minimum Unsatisfiable Core).
Consider the set of all unsatisfiable cores for a formula
ϕ : {ψ1, . . . , ψj}. Then, ψk ∈ {ψ1, . . . , ψj} is a minimum
unsatisfiable core iff ∀ ψi ∈ {ψ1, . . . , ψj}, 1 ≤ i ≤ j :
|ψk| ≤ |ψi|.
Preliminaries (con’t)
Definition 4. (Satisfiable Subformula).
Consider a formula ϕ, φ is a satisfiable subformula for ϕ iff φ
is a satisfiable formula and φ ⊆ ϕ.
Definition 5. (Maximal Satisfiable Subformula).
Given a satisfiable subformula φ for a formula ϕ, φ is a
maximal satisfiable subformula iff adding any clause
ω ∈ {ϕ − φ} into φ implies that φ ∪ {ω} is unsatisfiable
Definition 6. (Minimal Hitting Set).
Suppose C = {S1, ..., Sn} is a collection of sets. Then H is a
hitting set of C iff H ⊆ 1≤i≤n ∪ Si, and H ∩ Si != ∅ for each
i with 1 ≤ i ≤ n. H is a minimal hitting set iff ∀ R ⊂ H : R is
not a hitting set.
•C={ {M1, M2, A1}, {M1, A1, A2, M3}}. The minimal hitting
sets are {M1}, {A1}, {M2, A2}, {M2, M3}.
Preliminaries (con’t)
Lemma 1. A minimal unsatisfiable core for a formula
ϕ is a minimal hitting set of the complements of
maximal satisfiable subformulas for ϕ.
Definition 7. (Minimum Hitting Set).
Given a collection C of sets and the set of all hitting sets of C :
{H1, . . . , Hj}, then Hk ∈ {H1, . . . , Hj} is a minimum hitting set
iff ∀ Hi ∈ {H1, . . . , Hj}, 1 ≤ i ≤ j : |Hk| ≤ |Hi|.
Lemma 2. A minimum unsatisfiable core for a
formula ϕ is a minimum hitting set of the complements of maximal satisfiable subformulas for ϕ.
Example
CNF formula
ϕ = (x1) ∧(~x2) ∧(~x1 ∨ x2) ∧ (~x2 ∨ x3) ∧ (~x3) .
1
2
3
4
5
The SAT and UNSAT Solutions of ϕ
Maximal satisfiable subformulas
{2, 3, 4, 5} {1, 2, 4, 5} {1, 3, 5} {1, 3, 4}
Complements of MSSes
{1} {3} {2, 4} {2, 5}
Minimal unsatisfiable cores
{1, 2, 3} {1, 3, 4, 5}
Minimum unsatisfiable core
{1, 2, 3}
Extracting Minimum UC
generate all minimal UCs then
select the smallest one
GA Main idea
How it work?
natural
selection
populations of
candidate solution
evolve to
a better solution
GA definitions&operators
Genetic encoding.:
chromosome code of CoMSSes. For example, CoMSSes is S =
{1, 3, 4, 7}, then the corresponding binary genes are 1011001
Fitness function.:
f(S) = HS/|S|;
(HS :number of sets hit by some of the elements in S, and |S|
represents the cardinality of the set S.)
Crossover operator.:
S1 : {x1, x2, xk.,xm} ; S2:{y1, y2,yk.,ym}; the crossover offspring : S3 :
{x1,.,xk,yk+1,.ym},S4 : {y1,.,yk,xk+1,.xm}
Mutation operator.:
S1 = {x1, x2, . . . , xm}, S2 = {si | if i = k, si = ￢xi, else si = xi}. is the mutation
offspring of S1
Inversion operator.:
S1 = {x1, . , xk, xk+1, . , xl−1,xl, .. , xm}, then S2= {x1, .. , xl,
xl−1, . , xk+1, xk,. . . , xm}.is the inversion offspring of S1
Selection operator.:
use fitness function. We choose hit more sets and have smaller
cardinality than others
Greedy Genetic Algorithm
algorithm proceeds as follows:
1. Find all complements of maximal satisfiable subformulas for a formula ϕ;
2. Recode the clause number in CoMSSes to make the sets more compressed;
3. Adopt a greedy algorithm to derive two good near minimum unsatisfiable
cores as the initial parents. We incrementally solve this problem, removing
solutions as they are found to continue the search until all have been found;
4. Encode the sets of CoMSSes as binary vector and obtain the binary genes;
5. Apply the genetic operators, including crossover, mutation and inversion, to
the selected parents, in order to give birth to the offspring;
6. Recombine the offspring and current parents to form a new population,
and employ the selection operator to choose the best solutions as the new
parents;
7. If the upper limit of iterations is reached, or the minimum unsatisfiable
cores remain the same size for 10 successive offspring, stop and report the
best solution found. Otherwise go to the step 5.
More example
(DP-complete problems are both
NP-hard and coNP-hard).