Some ideas

[giuliojiang]

Structure

Create a special class for Func mode to store not only input CNFs, but also a (limited) history of corresponding mutations and their success (coverage percentage if we can get it). In this way we can have built-up of mutations where multiple strategies can collaborate on the same input.

Equivalent mutation

Mutation: Add p v ¬ps to existing clauses. They become automatically True so they effectively don't have any effect. SAT -> SAT, UNSAT -> UNSAT

Contradicting unit literals

Mutation: Add contradicting unit clauses (p) ^ (¬p). Makes the formula UNSAT.

Contradicting 2-clauses

Mutation: Add contradicting binary clauses in random places, with random variable numbers

1 2 0
-2 -1 0
1 -2 0
-1 2 0

1 2 0
-2 3 0
1 -2 0
-1 2 0
-1 -2 -3 0

Distribution

Equivalence transformation. Take 2 random clauses that have at least 2 literals. Distribute. Distribute again. Shuffle the clauses (each of them has 2 literals and are in DNF). Reconstruct 4 CNF clauses from pairs of DNF clauses.

[giuliojiang]

Pure literals injection

Inject lots of pure literals (either pick a new var or use an existing var) in existing clauses, to trigger pure literal processing code.

[giuliojiang]

BCP Unit Injection

Take an existing (p v q v ...) Transform that in (¬x v p v q v ...) ^ (x)

This triggers BCP