

![0_image_0.png](0_image_0.png)

GUNSAT operates on an initial formula ϕ through a few operations: 2-saturation, remove-one-clause, add-one-clause, add-extended-variables and *simplify-look-ahead*. Some of these operations depend on a powerful scoring scheme. A score is given to all pairs of literals based on their frequency appearance in the formula. Let us consider a clause ci of length ni. Each pair (l1,l2) appearing in ciis credited a weight of w2 (ni) = 2 n−1−n1 ni.(ni−1)
. The score of a pair of literals (l1,l2) is defined as the sum of its weights in all clauses and noted S(l1,l2). The score S(c) of a clause c is the sum of the scores of all the pairs of literals it contains.

The 2-saturation step ensures that, each time a new binary clause is added to ϕ, all resolution operations between the set of binary clauses are performed to saturate ϕ. In order to exploit their full power, an equivalency literal search is performed. While performing the binary clause saturation, the algorithm may find new unit clauses (note that in a resolution step between two binary clauses the resolvent can have either one or two literals). The literal l of the unit clause is then propagated in the whole formula by unit propagation. An inconsistency may be identified at this step and the algorithm returns UNSAT-ISFIABLE, proving the unsatisfiability of the formula. Refer to [3] for the use of binary clause saturation for preprocessing purposes.

In addition, if the size of the current formula is greater than a fixed *MaxSize* then a non-vital clause is removed by *remove-one-clause*. In each iteration there is also a call to *add-one-clause*, which adds one clause to the current formula according to the scoring scheme. Both *add-extended-variables* and simplify-look-ahead use reasoning mechanisms (extended resolution in the former, unit propagation lookahead in the latter) to improve the chances of deriving an empty clause in the next iteration. *Addextended-variables* adds the three clauses generated through extended resolution to the formula. *Simplifylook-ahead* applies unit propagation look-ahead to the formula [12], which may eventually conclude the formula is unsatisfiable.

Extended resolution is applied when the algorithm has tried to increase the score of a given pair of literals too many times without success, and it uses extended resolution to artificially increase that score.

The application of the extended rule implies adding a new variable e and three clauses to the formula. In