Full Disclosure mailing list archives
Re: help fuzzing/finding Horn CNF formula
From: Pavel Kankovsky <peak () argo troja mff cuni cz>
Date: Sun, 21 Feb 2010 16:38:29 +0100 (CET)
On Fri, 19 Feb 2010, Georgi Guninski wrote:
i am looking for a HORN CNF that is SAT if and only if |x != y| ($x \ne y$) for boolean x,y.
Lemma: Let F(x_1, x_2, ...) be a Horn formula and A a B vectors assigning truth values to its propositional variables x_1, .... If F is satisfied by both A and B then F is satisfied by A&B where (A&B)_i = A_i & B_i = min(A_i, B_i). Proof: Let C be any clause of F. It can be a fact, a rule or a constraint: 1. If C == x_i is a fact: both A_i and B_i must be 1, (A&B)_i = 1, therefore C is satisfied by A&B. 2. If C == ~x_i \/ ~x_j \/ ... \/ x_k is a rule: If (A&B)_k = 1 then C is satisfied by A&B. If (A&B)_k = 0 then A_k = 0 or B_k = 0. Let's assume A_k = 0 without loss of generality: C is satisfied by A therefore at least one of A_i, A_j, ... must be 0 too. This implies at least one of (A&B)_i, (A&B)_j, ... is 0 as well and C is satisfied by A&B. 3. If C = ~x_i \/ ~x_j \/ ... is a constraint: C is satisfied by A therefore at least one of A_i, A_j, ... must be 0. This implies at least one of (A&B)_i, (A&B)_j, ... is 0 as well and C is satisfied by A&B. QED. Consequence of lemma: Let F be a Horn formula satisfied by vectors (0, 1, A) and (1, 0, B). Then F is satisfied by (0, 0, A&B). In other words, there is no Horn formula F(x, y, ...) satisfiable if and only if x and y are assigned different truth values. This result does not contradict P-completeness of HORN-SAT because the transformation of the original problem is allowed to make changes to its input--such as to negate one of variables and turn a question of nonequivalence into a question of equivalence (expressible with a Horn formula). -- Pavel Kankovsky aka Peak / Jeremiah 9:21 \ "For death is come up into our MS Windows(tm)..." \ 21st century edition / _______________________________________________ Full-Disclosure - We believe in it. Charter: http://lists.grok.org.uk/full-disclosure-charter.html Hosted and sponsored by Secunia - http://secunia.com/
Current thread:
- help fuzzing/finding Horn CNF formula Georgi Guninski (Feb 19)
- Re: help fuzzing/finding Horn CNF formula Jeff Williams (Feb 19)
- Re: help fuzzing/finding Horn CNF formula Pavel Kankovsky (Feb 21)