Prev: Class of Total function is PRC Class ?
Next: A result from my work at the Perimeter Institute
From: translogi on 20 Jan 2008 12:25
Puzzeling about Satisfiabliity problems (that are problems
questioining if an propositional formulais satisfiable or not,
satisfiable meaning that there is a posibility of the formula being
true)

I found that a formula F in the form of

F <==> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
a1,a2,b1,b2,f1,f2,g1,g2,and x being propositional variables ,
Z being a formula


is equivalent to

({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)


And that if the formula Z does not contain x

(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z

is equi satisfiable with

({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z

A formula that does not contain the propositional variable x

If this formula is satisfiable x can be deduced from:
({[~a1.~a2]+[~b1.~b2]} -> x).
({[~f1.~f2]+[~g1.~g2]} -> ~x)
If neither of the antecedents are true x can be either true or false.



Proof of equivalence
(a1 +a2 +x).(b1 +b2 +x).(f1 +f2 +~x).(g1 +g2 +~x).Z
and
({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

starting with
(a1 +a2 +x).(b1 +b2 +x).(f1 +f2 +~x).(g1 +g2 +~x).Z

<==>
make implications -> x and -> ~x
(A+B) <==> (~A -> B)

(~{a1+a2} -> x).(~{b1+b2} -> x).(~{f1+f2} -> ~x).(~{g1+g2}-> ~x) .Z

<==>
to 2 implications
(A -> C).(B -> C) <==> ([A+B] -> C)

([~{a1 +a2} + ~{b1 +b2}] -> x).([~{f1 +f2} + ~{g1 +g2}] -> ~x) .Z

<==>
Transposition ( A-> ~B) <==> ( A-> ~B).(B -> ~A).

([~{a1+a2} + ~{b1+b2}] -> x).([~{f1+f2} + ~{g1+g2}] -> ~x).
(x -> ~[~{f1+f2} + ~{g1+g2}]).Z

<==>
Add Hypothetical syllogism (A -> B).(B-> C) <==> (A -> C).(A -> B).(B-
> C)

([~{a1 +a2} + ~{b1 +b2}] -> ~[~{f1 +f2} + ~{g1 +g2}]).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

<==>
convert implication to disjunction
(A -> B) <==> (~A+B)

(~[~{a1+a2} + ~{b1+b2}] + ~[~{f1 +f2} + ~{g1 +g2}]).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

<==>
De Morgan simplification on first line ~(~A +~B) <==> (A.B)

([{a1+a2}.{b1+b2}] + [{f1 + f2}.{g1 + g2}]).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

<==>
To CNF (distribution . over +) (P + [F.G]) <--> (P+F).(P+G)

([{a1+a2}.{b1+b2}]+ {f1 + f2}) .([{a1+a2}.{b1+b2}]+ {g1 + g2}).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

<==>
To CNF(distribution . over +) ([A.B] + F]) <--> (A+F).(B+F)
({a1+a2}+{f1+f2}).({b1+b2}+{f1+f2}).
({a1+a2}+{g1+g2}).({b1+b2}+{g1+g2}).
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

<==> reshuffeling clauses (A.B ) <==> (B.A)
({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)

the other way around is all the steps in the reverse direction.
(they are all equivalences)


I am not able to proof that if the formula Z does not contain x

(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z

is equi satisfiable with
({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z

But i did some tests.
and it looks all right.
(formula's that were insatisfiable kept being insatisfiable, formula's
that were satisfiable stayed satisfiable)

(I just don't know how to formaly to proof equisatisfiability)


From: herbzet on 22 Jan 2008 03:34


translogi wrote:
>
> Puzzeling about Satisfiabliity problems (that are problems
> questioining if an propositional formulais satisfiable or not,
> satisfiable meaning that there is a posibility of the formula being
> true)
>
> I found that a formula F in the form of
>
> F <==> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
> a1,a2,b1,b2,f1,f2,g1,g2,and x being propositional variables ,
> Z being a formula
>
> is equivalent to
>
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)
>
> And that if the formula Z does not contain x
>
> (a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z

This formula is F, as per above.

> is equi satisfiable with
>
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
>
> A formula that does not contain the propositional variable x

Call this formula G.

Long story short: F -> G is a tautology. G -> F is not a tautology.

> If this formula is satisfiable x can be deduced from:
> ({[~a1.~a2]+[~b1.~b2]} -> x).
> ({[~f1.~f2]+[~g1.~g2]} -> ~x)
> If neither of the antecedents are true x can be either true or false.

Not sure what the above four lines are saying.

> Proof of equivalence
> (a1 +a2 +x).(b1 +b2 +x).(f1 +f2 +~x).(g1 +g2 +~x).Z
> and
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z
>
> starting with
> (a1 +a2 +x).(b1 +b2 +x).(f1 +f2 +~x).(g1 +g2 +~x).Z
>
> <==>
> make implications -> x and -> ~x
> (A+B) <==> (~A -> B)
>
> (~{a1+a2} -> x).(~{b1+b2} -> x).(~{f1+f2} -> ~x).(~{g1+g2}-> ~x) .Z

Right.

> <==>
> to 2 implications
> (A -> C).(B -> C) <==> ([A+B] -> C)
>
> ([~{a1 +a2} + ~{b1 +b2}] -> x).([~{f1 +f2} + ~{g1 +g2}] -> ~x) .Z

Right.

> <==>
> Transposition ( A-> ~B) <==> ( A-> ~B).(B -> ~A).
>
> ([~{a1+a2} + ~{b1+b2}] -> x).([~{f1+f2} + ~{g1+g2}] -> ~x).
> (x -> ~[~{f1+f2} + ~{g1+g2}]).Z

Right.

> <==>
> Add Hypothetical syllogism (A -> B).(B-> C) <==> (A -> C).(A -> B).(B-
> > C)
>
> ([~{a1 +a2} + ~{b1 +b2}] -> ~[~{f1 +f2} + ~{g1 +g2}]).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z

Right. The first line is a consequence of, but not equivalent to,
the second line. The second line is equivalent to F. Call it F'.
The variable x has been eliminated in the first line, as has Z.

Now we reduce the first line to CNF:

> <==>
> convert implication to disjunction
> (A -> B) <==> (~A+B)
>
> (~[~{a1+a2} + ~{b1+b2}] + ~[~{f1 +f2} + ~{g1 +g2}]).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z
>
> <==>
> De Morgan simplification on first line ~(~A +~B) <==> (A.B)
>
> ([{a1+a2}.{b1+b2}] + [{f1 + f2}.{g1 + g2}]).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z
>
> <==>
> To CNF (distribution . over +) (P + [F.G]) <--> (P+F).(P+G)
>
> ([{a1+a2}.{b1+b2}]+ {f1 + f2}) .([{a1+a2}.{b1+b2}]+ {g1 + g2}).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z
>
> <==>
> To CNF(distribution . over +) ([A.B] + F]) <--> (A+F).(B+F)
> ({a1+a2}+{f1+f2}).({b1+b2}+{f1+f2}).
> ({a1+a2}+{g1+g2}).({b1+b2}+{g1+g2}).
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x).Z
>
> <==> reshuffeling clauses (A.B ) <==> (B.A)
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)

This is G & F' (after condensing Z & Z to Z).

> the other way around is all the steps in the reverse direction.
> (they are all equivalences)

Right. So F = (G & F') [allowing that (Z & Z) = Z].

> I am not able to proof that if the formula Z does not contain x
>
> (a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z
>
> is equi satisfiable with
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z

The first formula is satisfiable iff Z is consistent with
the other four conjuncts.

The second formula is a consequence of the first formula, so
any truth-assignment that satisfies the first will satisfy
the second.

> But i did some tests.
> and it looks all right.
> (formula's that were insatisfiable kept being insatisfiable, formula's
> that were satisfiable stayed satisfiable)
>
> (I just don't know how to formaly to proof equisatisfiability)

From what you say it seems to me that two formulae are equi-
satisfiable iff they are both contradictions or both not
contradictions.

Neither of the formulae in question above is a contradiction
unless Z is incompatible with the other conjuncts.

If Z = (~a1 & ~a2 & ~x) then the first formula is a contradiction
but the second formula is satisfiable,

I don't think that the first formula can be a contradiction,
but the second satisfiable, if Z does not contain x as a
(relevant) variable, but I don't have proof at the moment.

--
hz
From: Jan on 22 Jan 2008 10:50
On 20 Jan., 18:25, translogi <wilem...(a)googlemail.com> wrote:
> Puzzeling about Satisfiabliity problems (that are problems
> questioining if an propositional formulais satisfiable or not,
> satisfiable meaning that there is a posibility of the formula being
> true)
>
> I found that a formula F in the form of
>
> F <==> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
> a1,a2,b1,b2,f1,f2,g1,g2,and x being propositional variables ,
> Z being a formula
>
> is equivalent to
>
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
> ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)
>
> And that if the formula Z does not contain x
>
> (a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z
>
> is equi satisfiable with
>
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
> ...
Resolving variables in a formula like this dates back to ~1960
Check out: http://en.wikipedia.org/wiki/Davis-Putnam_algorithm
Regards Jan



From: translogi on 22 Jan 2008 12:35
On Jan 22, 3:50 pm, Jan <j...(a)daimi.au.dk> wrote:
> On 20 Jan., 18:25, translogi <wilem...(a)googlemail.com> wrote:
>
>
>
> > Puzzeling about Satisfiabliity problems (that are problems
> > questioining if an propositional formulais satisfiable or not,
> > satisfiable meaning that there is a posibility of the formula being
> > true)
>
> > I found that a formula F in the form of
>
> > F <==> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
> > a1,a2,b1,b2,f1,f2,g1,g2,and x being propositional variables ,
> > Z being a formula
>
> > is equivalent to
>
> > ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> > ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
> > ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2}  + {~g1.~g2}] -> ~x)
>
> > And that if the formula Z does not contain x
>
> > (a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z
>
> > is equi satisfiable with
>
> > ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> > ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
> > ...
>
> Resolving variables in a formula like this dates back to ~1960
> Check out:http://en.wikipedia.org/wiki/Davis-Putnam_algorithm
> Regards Jan- Hide quoted text -
>
> - Show quoted text -

Think there is a difference between "my" theorem and the DPLL
algorithm.

The DPLL algoritm is more a trial and error algorithm while in using
"my" theorem there is no backtracking.at all.

only after an model in which
({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
is true

is found
x can be decided but this has no influence anymore on the truth value
of

with
({[~a1.~a2]+[~b1.~b2]} -> x).
({[~f1.~f2]+[~g1.~g2]} -> ~x)

Both antecedents cannot both be true
If both antecedents are false x is indetermend.


and
{(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
is true as well.


also if

({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
is unsatisfiable

then
{(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z} is unsatisfiable as
well.
independent on the truth value of x

This all only if Z does not contain a meaningfull / relevant x.
(no clauses only containing x or ~x, if a clause contains them both it
is not a meaningfull clause but a tautology)


But maybe this all comes from me not having full knowledge of the DPLL
algorithm.

Do you know how to formaly proof equi satisfiability between two
formulas?



From: Jan on 22 Jan 2008 16:50
On 22 Jan., 18:35, translogi <wilem...(a)googlemail.com> wrote:
> On Jan 22, 3:50 pm, Jan <j...(a)daimi.au.dk> wrote:
>
>
>
> > On 20 Jan., 18:25, translogi <wilem...(a)googlemail.com> wrote:
>
> > > Puzzeling about Satisfiabliity problems (that are problems
> > > questioining if an propositional formulais satisfiable or not,
> > > satisfiable meaning that there is a posibility of the formula being
> > > true)
>
> > > I found that a formula F in the form of
>
> > > F <==> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
> > > a1,a2,b1,b2,f1,f2,g1,g2,and x being propositional variables ,
> > > Z being a formula
>
> > > is equivalent to
>
> > > ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> > > ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z.
> > > ([{~a1.~a2} + {~b1.~b2}] -> x).([{~f1.~f2} + {~g1.~g2}] -> ~x)
>
> > > And that if the formula Z does not contain x
>
> > > (a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z
>
> > > is equi satisfiable with
>
> > > ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> > > ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
> > > ...
>
> > Resolving variables in a formula like this dates back to ~1960
> > Check out:http://en.wikipedia.org/wiki/Davis-Putnam_algorithm
> > Regards Jan- Hide quoted text -
>
> > - Show quoted text -
>
> Think there is a difference between "my" theorem and the DPLL
> algorithm.
>
> The DPLL algoritm is more a trial and error algorithm while in using
> "my" theorem there is no backtracking.at all.
>
> only after an model in which
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
> is true
>
> is found
> x can be decided but this has no influence anymore on the truth value
> of
>
> with
> ({[~a1.~a2]+[~b1.~b2]} -> x).
> ({[~f1.~f2]+[~g1.~g2]} -> ~x)
>
> Both antecedents cannot both be true
> If both antecedents are false x is indetermend.
>
> and
> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z}
> is true as well.
>
> also if
>
> ({a1+a2}+{f1+f2}).({a1+a2}+{g1+g2}).
> ({b1+b2}+{f1+f2}).({b1+b2}+{g1+g2}).Z
> is unsatisfiable
>
> then
> {(a1+a2+x).(b1+b2+x).(f1+f2+~x).(g1+g2+~x).Z} is unsatisfiable as
> well.
> independent on the truth value of x
>
> This all only if Z does not contain a meaningfull / relevant x.
> (no clauses only containing x or ~x, if a clause contains them both it
> is not a meaningfull clause but a tautology)
>
> But maybe this all comes from me not having full knowledge of the DPLL
> algorithm.
>
> Do you know how to formaly proof equi satisfiability between two
> formulas?

Be careful no to confuse the original Davis-Putnam algorithm with
DPLL.

The Davis-Putnam algorithm is solely based on "resolution" - with one
catch - the formulae will generally grow exponential with respect to
the number of clauses.

DPLL uses a refined "resolution" algorithm as part of the solving
algorithm.
"Resolution" in DPLL is only used when the number of occurrences for a
variable x and its negations holds a specific property - can you find
that property? (your example complies with it)
By using the refinement, a formula will in the worst case be constant
in size with respect to the numbers of clause but with one variable
less.

Regards Jan



 |  Next  |  Last
Pages: 1 2
Prev: Class of Total function is PRC Class ?
Next: A result from my work at the Perimeter Institute