Affine Formulas

A propositional formula is said to be affine (or in XOR-CNF) [Sch78,KS98,Zan02] if it is written as a finite conjunction of linear equations over the two-element field, e.g., $\phi=(x_1\oplus x_3=1)\wedge(x_1\oplus x_2\oplus x_4=0)$. As can be seen, equations play the same role in affine formulas as clauses do in CNFs; roughly, affine formulas represent conjunctions of parity or equivalence constraints. This class proves interesting for knowledge representation, since on one hand it is tractable for most of the common reasoning tasks, and on the other hand the affine approximations of a knowledge base can be made very small and are efficiently learnable [Zan02]. We show that projecting an affine formula onto a subset of its variables is quite easy too, enabling our algorithm to run in polynomial time. The proof of the following lemma is easily obtained with gaussian elimination [CUR84]: triangulate $\phi$ with the variables in $A$ put rightmost, and then keep only those equations formed upon $A$; full details are given in the technical report version [Zan03].

Lemma 1   Let $\phi$ be an affine formula containing $k$ equations, and $A\subseteq Var(\phi)$. Then an affine formula $\psi$ with ${\mathcal M}(\psi)=({\mathcal M}(\phi))_{\vert A}$ and containing at most $k$ equations can be computed in time $O(k^2\vert Var(\phi)\vert)$.

Proposition 2   If $\Sigma$ is represented by an affine formula containing $k$ equations and $\alpha$ by a disjunction of $k'$ linear equations, and $A$ is a subset of $Var(\Sigma)$, then searching for a best explanation for $\Pi=(\Sigma,\alpha,A)$ can be done in time $O((k+k')((k+1)^2+\vert A\vert(k+k'))n)$.

Sketch of proof It is easily seen that an affine formula (containing $k'+k$ equations and $n$ variables) for $\Sigma\wedge\overline{\alpha}$ can be computed in time linear in the size of $\alpha$; this formula can be projected onto $A$ in time $O((k+k')^2n)$, and we straightforwardly get a disjunction of at most $k+k'$ linear equations for $\overline{({\mathcal M}(\Sigma\wedge\overline{\alpha}))_{\vert A}}$. Then we can use distributivity of $\wedge$ over $\vee$ for solving the satisfiability problem of the algorithm; recall that SAT can be solved in time $O(k^2n)$ for an affine formula of $k$ equations over $n$ variables by the elimination method of Gauss [CUR84]. The remaining operations are straightforward. $\square$

Note that variables, literals and clauses are special cases of disjunctions of linear equations.