diff --git a/versions/z3-crsat-0.01.txt b/versions/z3-crsat-0.01.txt deleted file mode 100644 index 49e1a1525..000000000 --- a/versions/z3-crsat-0.01.txt +++ /dev/null @@ -1,12 +0,0 @@ -More focused (_FOCUS_ == 2) WalkSAT version. -Variables are chosen among candidates in only one unsatisfied bit-vector term. -Flip rate slightly slower; probably due to larger hash-table and recursive formula structure. -No restarts. - -#define _CNF_ 0 -#define _BFS_ 1 -#define _FOCUS_ 3 -#define _RESTARTS_ 0 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-gsat-0.01.txt b/versions/z3-gsat-0.01.txt deleted file mode 100644 index eb806a67f..000000000 --- a/versions/z3-gsat-0.01.txt +++ /dev/null @@ -1,10 +0,0 @@ -Basic GSAT version. -No restarts. - -#define _CNF_ 0 -#define _BFS_ 0 -#define _FOCUS_ 0 -#define _RESTARTS_ 0 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-gsat-res-0.01.txt b/versions/z3-gsat-res-0.01.txt deleted file mode 100644 index 6a211f2bc..000000000 --- a/versions/z3-gsat-res-0.01.txt +++ /dev/null @@ -1,10 +0,0 @@ -Basic GSAT version corresponding to Christoph's original code. -Restarts after 100 plateaus. - -#define _CNF_ 0 -#define _BFS_ 0 -#define _FOCUS_ 0 -#define _RESTARTS_ 1 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01.txt b/versions/z3-wsat-0.01.txt deleted file mode 100644 index fec38518d..000000000 --- a/versions/z3-wsat-0.01.txt +++ /dev/null @@ -1,14 +0,0 @@ -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. \ No newline at end of file diff --git a/versions/z3-wsat-0.01b.txt b/versions/z3-wsat-0.01b.txt deleted file mode 100644 index 8bcf2ffeb..000000000 --- a/versions/z3-wsat-0.01b.txt +++ /dev/null @@ -1,14 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion. -Chooses a random top level assertion instead of using a BFS approach (_BFS_ == 0). -No restarts. - -#define _CNF_ 0 -#define _BFS_ 0 -#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. \ No newline at end of file diff --git a/versions/z3-wsat-0.01c.txt b/versions/z3-wsat-0.01c.txt deleted file mode 100644 index 223560e08..000000000 --- a/versions/z3-wsat-0.01c.txt +++ /dev/null @@ -1,12 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion. -AND is scored by average; OR is scored by inverse multiplication. -No restarts. - -#define _CNF_ 0 -#define _BFS_ 1 -#define _FOCUS_ 1 -#define _RESTARTS_ 0 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 1 -#define _SCORE_OR_MUL_ 1 \ No newline at end of file diff --git a/versions/z3-wsat-0.01d.txt b/versions/z3-wsat-0.01d.txt deleted file mode 100644 index 072191370..000000000 --- a/versions/z3-wsat-0.01d.txt +++ /dev/null @@ -1,11 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion with MINIMAL top_score. -No restarts. - -#define _CNF_ 0 -#define _BFS_ 2 -#define _FOCUS_ 1 -#define _RESTARTS_ 0 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.01e.txt b/versions/z3-wsat-0.01e.txt deleted file mode 100644 index b018c5e0d..000000000 --- a/versions/z3-wsat-0.01e.txt +++ /dev/null @@ -1,11 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion with MAXIMAL top_score. -No restarts. - -#define _CNF_ 0 -#define _BFS_ 3 -#define _FOCUS_ 1 -#define _RESTARTS_ 0 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file diff --git a/versions/z3-wsat-0.02.txt b/versions/z3-wsat-0.02.txt deleted file mode 100644 index 34dcb157c..000000000 --- a/versions/z3-wsat-0.02.txt +++ /dev/null @@ -1,13 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion. -Score function reduced to 0/1. -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 -#define _WEIGHTED_DIST_ 1 \ No newline at end of file diff --git a/versions/z3-wsat-res-0.01.txt b/versions/z3-wsat-res-0.01.txt deleted file mode 100644 index 575180a59..000000000 --- a/versions/z3-wsat-res-0.01.txt +++ /dev/null @@ -1,13 +0,0 @@ -Basic WalkSAT version. -Variables are chosen among candidates in only ONE top level assertion. -Flip rate increased by roughly 10%-300% compared to GSAT. -Restarts after 100 plateaus. -Fps slightly decreased due to restarts. - -#define _CNF_ 0 -#define _BFS_ 1 -#define _FOCUS_ 1 -#define _RESTARTS_ 1 -#define _TIMELIMIT_ 300 -#define _SCORE_AND_AVG_ 0 -#define _SCORE_OR_MUL_ 0 \ No newline at end of file