mirror of
https://github.com/Z3Prover/z3
synced 2025-07-16 17:36:39 +00:00
14 lines
No EOL
372 B
Text
14 lines
No EOL
372 B
Text
Basic WalkSAT version.
|
|
Variables are chosen among candidates in only ONE top level assertion.
|
|
Flip rate increased by roughly 10%-300%.
|
|
No restarts.
|
|
|
|
#define _CNF_ 0
|
|
#define _BFS_ 1
|
|
#define _FOCUS_ 1
|
|
#define _RESTARTS_ 0
|
|
#define _TIMELIMIT_ 300
|
|
#define _SCORE_AND_AVG_ 0
|
|
#define _SCORE_OR_MUL_ 0
|
|
|
|
BUGGY VERSION! Uses wrong value for modulo operation in assertion selection. |