Next: DNFs Up: Polynomial Classes Previous: Polynomial Classes

## 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., . 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 with the variables in put rightmost, and then keep only those equations formed upon ; full details are given in the technical report version [Zan03].

Lemma 1   Let be an affine formula containing equations, and . Then an affine formula with and containing at most equations can be computed in time .

Proposition 2   If is represented by an affine formula containing equations and by a disjunction of linear equations, and is a subset of , then searching for a best explanation for can be done in time .

Sketch of proof It is easily seen that an affine formula (containing equations and variables) for can be computed in time linear in the size of ; this formula can be projected onto in time , and we straightforwardly get a disjunction of at most linear equations for . Then we can use distributivity of over for solving the satisfiability problem of the algorithm; recall that SAT can be solved in time for an affine formula of equations over variables by the elimination method of Gauss [CUR84]. The remaining operations are straightforward.

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

Next: DNFs Up: Polynomial Classes Previous: Polynomial Classes
Bruno Zanuttini 2003-06-30