mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

BV-SLS final integration.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-20 15:19:31 +00:00
parent 61ba7f5e09
commit 074ff311c0
10 changed files with 0 additions and 120 deletions
Download patch file Download diff file Expand all files Collapse all files

12
versions/z3-crsat-0.01.txt
View file

@ -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

10
versions/z3-gsat-0.01.txt
View file

@ -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

10
versions/z3-gsat-res-0.01.txt
View file

@ -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

14
versions/z3-wsat-0.01.txt
View file

@ -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.

14
versions/z3-wsat-0.01b.txt
View file

@ -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.

12
versions/z3-wsat-0.01c.txt
View file

@ -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

11
versions/z3-wsat-0.01d.txt
View file

@ -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

11
versions/z3-wsat-0.01e.txt
View file

@ -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

13
versions/z3-wsat-0.02.txt
View file

@ -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

13
versions/z3-wsat-res-0.01.txt
View file

@ -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