An Evolutionary Local Search Method for Incremental Satisfiability - Artificial Intelligence and Symbolic Computation - page 150

Algorithm τ-EO-ISAT
If S satisfies

ϕ then Return ϕ ∪ ϕ is satisfiable.

S P S

{}

1. ϕ = C

S

a. X ∩ X = φ

ϕ C

P

A model for C is found by assigning the truth value 1 or 0 to one

positive or negative literal, respectively. Return that ϕ ∪ ϕ is satisfiable.

P S

( ) ( )

b. X ∩ X ≠ φ and X ⊄ X

ϕ C C ϕ

P P

Assign the truth value 1 or 0 to one positive or negative literal of

X C − X , respectively. Return that ϕ ∪ ϕ is satisfiable.

ϕ P S

P

c. X C ⊆ X

ϕ

P

Determine ϕ .

P

Call τ-EO-SAT with Variables = X and Clauses = ϕ ∪ C . The initial

ϕ P 1

P 1

solution of the algorithm is the assignment S to the variables X ϕ and the

P 1

variable fitness λ is given by Equation 9.

i

If ϕ ∪ C is satisfiable then Return that ϕ ∪ ϕ is satisfiable Else Return

P 1 P S

that no model can be found.

{ }

2. ϕ = C , C ,..., C

S 1 2 p

a. X ∩ X = φ

ϕ ϕ

P S

Call τ-EO-SAT with Variables = X and Clauses = ϕ .

ϕ S

S

If S ϕ is satisfiable then Return that ϕ ∪ ϕ is satisfiable Else Return that no

P S

model can be found.

b. X ∩ X ≠ φ

ϕ ϕ

P S

.
(i) Call τ-EO-SAT with

Determine ϕ , ϕ , ϕ

P 1 S 1 S 2

Variables = X and Clauses = ϕ .

S 2

ϕ

S 2

If no model can be found for ϕ then Return that no model can be

S 2

found for ϕ ∪ ϕ .

P S

(ii) Call τ .

1. The algorithm starts with the assignment S to the variables

-EO-SAT with Variables = X ∪ X and Clauses = ϕ ∪ ϕ

ϕ ϕ P 1 S 1

P 1 S 1

X ϕ and random Boolean values to X ϕ . If ϕ ∪ ϕ is satisfi-

P 1 S 1

P 1 S 1

is satisfiable.
2. The algorithm starts with completely randomly generated as-
signment where the variable fitness

able then Return that ϕ ∪ ϕ

P S

λ is given by Eqn. 9. If

i

ϕ ∪ ϕ is satisfiable then Return that ϕ ∪ ϕ is satisfiable

P 1 S 1 P S

Else Return that no model can be found for ϕ ∪ ϕ .

P S

End τ-EO-ISAT

Fig. 2. Genericτ-EO algorithm for ISAT