Slider 40:
Code
Put this as an attachment (icon)
p bdd 62 65
#define add_state1(1, 3, 15, 7, 19, 20)
#equ(xor3(1, and(-7, 3), nand(20, 19), ite(15, or(3, -20), -3)))
1. add_state1(1, 3, 15, 7, 19, 20)
2. add_state1(2, 4, 16, 8, 20, 21)
3. add_state1(3, 5, 17, 9, 21, 22)
4. add_state1(4, 6, 18, 10, 22, 23)
5. add_state1(5, 7, 19, 11, 23, 24)
6. add_state1(6, 8, 20, 12, 24, 25)
7. add_state1(7, 9, 21, 13, 25, 26)
8. add_state1(8, 10, 22, 14, 26, 27)
9. add_state1(9, 11, 23, 15, 27, 28)
10. add_state1(10, 12, 24, 16, 28, 29)
11. add_state1(11, 13, 25, 17, 29, 30)
12. add_state1(12, 14, 26, 18, 30, 31)
13. add_state1(13, 15, 27, 19, 31, 32)
14. add_state1(14, 16, 28, 20, 32, 33)
15. add_state1(15, 17, 29, 21, 33, 34)
16. add_state1(17, 19, 31, 23, 35, 36)
17. add_state1(18, 20, 32, 24, 36, 37)
18. add_state1(19, 21, 33, 25, 37, 38)
19. add_state1(20, 22, 34, 26, 38, 39)
#define add_state2(1, 2, 6, 13, 17, 20)
#xor3(-1, xor3(6, and(-13, 17), 13), equ(20, 2))
#define add_state3(1, 2, 6, 13, 17, 20)
#not(xor3(-1, xor3(6, and(-13, 17), 13), equ(20, 2)))
20. add_state2(1, 2, 6, 13, 17, 20)
21. add_state3(2, 3, 7, 14, 18, 21)
22. add_state2(3, 4, 8, 15, 19, 22)
23. add_state3(4, 5, 9, 16, 20, 23)
24. add_state2(5, 6, 10, 17, 21, 24)
25. add_state3(6, 7, 11, 18, 22, 25)
26. add_state2(7, 8, 12, 19, 23, 26)
27. add_state3(8, 9, 13, 20, 24, 27)
28. add_state2(9, 10, 14, 21, 25, 28)
29. add_state3(10, 11, 15, 22, 26, 29)
30. add_state2(11, 12, 16, 23, 27, 30)
31. add_state3(12, 13, 17, 24, 28, 31)
32. add_state2(13, 14, 18, 25, 29, 32)
33. add_state3(14, 15, 19, 26, 30, 33)
34. add_state2(15, 16, 20, 27, 31, 34)
35. add_state3(16, 17, 21, 28, 32, 35)
36. add_state2(17, 18, 22, 29, 33, 36)
37. add_state3(18, 19, 23, 30, 34, 37)
38. add_state2(19, 20, 24, 31, 35, 38)
39. add_state3(20, 21, 25, 32, 36, 39)
Notes:
;add_state2(5, 6, 10, 17, 21, 24) ; jumped to 8 solutions adding 5
// used to comment out line and determining data
exist(add_state2(5, 6, 10, 17, 21, 24), 17)
//delete variable from a line
Command Line Arguments:
./sbsat slider_40_sat.ite --break-xors 0 -L 0 -All 0 --max-solutions 0
Why did I start this way?
Get a feel for where I can start narrowing down and analyzing to eliminate variables, for example now I can analyze line 1 because it is a different amount of solutions from the majority.
DATA:
1.)OBTAIN DATA
Commenting Line # / Time / Choice Points / Backtracks / Number Solutions / Satisfiable?None / 0.129 / 749 / 750 / 3/0 / Yes (3)
1 / 0.130 / 809 / 810 / 4/0 / Yes (4)
2 / 0.131 / 864 / 865 / 3/0 / Yes (3)
3 / 0.136 / 809 / 810 / 3/0 / Yes (3)
4 / 0.130 / 832 / 833 / 3/0 / Yes (3)
5 / 0.131 / 838 / 839 / 3/0 / Yes (3)
6 / 0.130 / 894 / 895 / 3/0 / Yes (3)
7 / 0.131 / 869 / 870 / 3/0 / Yes (3)
8 / 0.130 / 891 / 892 / 3/0 / Yes (3)
9 / 0.130 / 842 / 843 / 3/0 / Yes (3)
10 / 0.132 / 832 / 833 / 3/0 / Yes (3)
11 / 0.129 / 871 / 872 / 3/0 / Yes (3)
12 / 0.130 / 844 / 845 / 4/0 / Yes (4)
13 / 0.134 / 946 / 947 / 3/0 / Yes (3)
14 / 0.129 / 873 / 874 / 3/0 / Yes (3)
15 / 0.131 / 882 / 883 / 3/0 / Yes (3)
16 / 0.130 / 885 / 886 / 3/0 / Yes (3)
17 / 0.129 / 861 / 862 / 3/0 / Yes (3)
18 / 0.137 / 854 / 855 / 3/0 / Yes (3)
19 / 0.134 / 810 / 811 / 4/0 / Yes (4)
20 / 0.143 / 928 / 929 / 3/0 / Yes (3)
21 / 0.130 / 828 / 829 / 4/0 / Yes (4)
22 / 0.136 / 820 / 821 / 3/0 / Yes (3)
23 / 0.129 / 775 / 776 / 3/0 / Yes (3)
24 / 0.143 / 822 / 823 / 3/0 / Yes (3)
25 / 0.137 / 824 / 825 / 3/0 / Yes (3)
26 / 0.128 / 814 / 815 / 3/0 / Yes (3)
27 / 0.129 / 804 / 805 / 3/0 / Yes (3)
28 / 0.130 / 856 / 857 / 6/0 / Yes (6)
29 / 0.130 / 795 / 796 / 5/0 / Yes (5)
30 / 0.129 / 806 / 807 / 5/0 / Yes (5)
31 / 0.131 / 806 / 807 / 3/0 / Yes (3)
32 / 0.127 / 840 / 841 / 4/0 / Yes(4)
33 / 0.128 / 807 / 808 / 3/0 / Yes (3)
34 / 0.128 / 871 / 872 / 3/0 / Yes (3)
35 / 0.147 / 770 / 771 / 3/0 / Yes (3)
36 / 0.158 / 809 / 810 / 3/0 / Yes (3)
37 / 0.142 / 767 / 768 / 4/0 / Yes (4)
38 / 0.144 / 782 / 783 / 3/0 / Yes (3)
39 / 0.152 / 766 / 767 / 3/0 / Yes (3)
2.) ISOLATE UNSUAL RESULTS
Time / ChoicePoints / Backtracks / Number Solutions / Satisfiable?
None / 0.129 / 749 / 750 / 3/0 / Yes (3)
1 / add_state1(13, 15, 27, 19, 31, 32) / 0.134 / 946 / 947 / 3/0 / Yes (3)
12 / add_state2(1, 2, 6, 13, 17, 20) / 0.143 / 928 / 929 / 3/0 / Yes (3)
13 / add_state3(2, 3, 7, 14, 18, 21) / 0.130 / 828 / 829 / 4/0 / Yes (4)
20 / add_state3(4, 5, 9, 16, 20, 23) / 0.129 / 775 / 776 / 3/0 / Yes (3)
21 / add_state2(9, 10, 14, 21, 25, 28) / 0.130 / 856 / 857 / 6/0 / Yes (6)
23 / add_state3(10, 11, 15, 22, 26, 29) / 0.130 / 795 / 796 / 5/0 / Yes (5)
28 / add_state2(11, 12, 16, 23, 27, 30) / 0.129 / 806 / 807 / 5/0 / Yes (5)
29 / add_state2(13, 14, 18, 25, 29, 32) / 0.127 / 840 / 841 / 4/0 / Yes(4)
30 / add_state3(16, 17, 21, 28, 32, 35) / 0.147 / 770 / 771 / 3/0 / Yes (3)
32 / add_state2(17, 18, 22, 29, 33, 36) / 0.158 / 809 / 810 / 3/0 / Yes (3)
35 / add_state3(18, 19, 23, 30, 34, 37) / 0.142 / 767 / 768 / 4/0 / Yes (4)
36 / add_state2(19, 20, 24, 31, 35, 38) / 0.144 / 782 / 783 / 3/0 / Yes (3)
37 / add_state3(20, 21, 25, 32, 36, 39) / 0.152 / 766 / 767 / 3/0 / Yes (3)
38 / add_state2(19, 20, 24, 31, 35, 38) / 0.144 / 782 / 783 / 3/0 / Yes (3)
39 / add_state3(20, 21, 25, 32, 36, 39) / 0.152 / 766 / 767 / 3/0 / Yes (3)
Taking out Variables:
Analysis
- sbsat was satisfiable for each line that was commented
Possible Questions:
What are Clauses?
Correlation between number of solns, choice points, backtracks
Need a refresher on choice points and backtracks
Shouldn’t time and number of choicepoints/backtracks be directly proportional?
Why was choice points one less than backtracks? optimization
None / 0.129 / 749 / 750 / 3/0 / Yes (3)exist( add_state2(1, 3, 15, 7, 19, 20), 1);
2 / 877 / 878
1 / 0.130 / 809 / 810 / 4/0 / Yes (4)
exist( add_state2(1, 3, 15, 7, 19, 20), 1);
2 / 0.145 / 877 / 878 / 4/0 / Yes(4)
3 / 0.128 / 880 / 881 / 4/0 / Yes(4)
2 + 3 / 0.131 / 881 / 882 / 5/0 / Yes(5)
12 / 0.130 / 844 / 845 / 4/0 / Yes (4)
13 / 0.134 / 946 / 947 / 3/0 / Yes (3)
20 / 0.143 / 928 / 929 / 3/0 / Yes (3)
21 / 0.130 / 828 / 829 / 4/0 / Yes (4)
28 / 0.130 / 856 / 857 / 6/0 / Yes (6)
29 / 0.130 / 795 / 796 / 5/0 / Yes (5)
30 / 0.129 / 806 / 807 / 5/0 / Yes (5)
32 / 0.127 / 840 / 841 / 4/0 / Yes(4)
35 / 0.147 / 770 / 771 / 3/0 / Yes (3)
36 / 0.158 / 809 / 810 / 3/0 / Yes (3)
37 / 0.142 / 767 / 768 / 4/0 / Yes (4)
38 / 0.144 / 782 / 783 / 3/0 / Yes (3)
39 / 0.152 / 766 / 767 / 3/0 / Yes (3)
Removing Clauses:
-Convert into CNF
- Use normal command line –c (prints to screen)
-Output to file
-Comment line to comment out the clause
- c line
- line always ends with 0
Core:
-if more solns, then most likely part of the core
-use exist to eliminate variables from lines that may be part of the core
Data:
-analyze
- relate variables in each of the lines
- relate results to entire file
Variables:
-if 3 variables were important they were in
ANALYSIS:
Addstate number:
Variable position:
Variable amount:
STEP 3: CHECKING VARIABLE AMOUNT & ANALYZING
add_state1(1, 3, 15, 7, 19, 20)add_state1(12, 14, 26, 18, 30, 31)
add_state1(13, 15, 27, 19, 31, 32)
add_state2(1, 2, 6, 13, 17, 20)
add_state3(2, 3, 7, 14, 18, 21)
add_state3(4, 5, 9, 16, 20, 23)
add_state2(9, 10, 14, 21, 25, 28)
add_state3(10, 11, 15, 22, 26, 29)
add_state2(11, 12, 16, 23, 27, 30)
add_state2(13, 14, 18, 25, 29, 32)
add_state3(16, 17, 21, 28, 32, 35)
add_state2(17, 18, 22, 29, 33, 36)
add_state3(18, 19, 23, 30, 34, 37)
add_state2(19, 20, 24, 31, 35, 38)
add_state3(20, 21, 25, 32, 36, 39)
Variable / Number of Times / Anne’s Results: Used to compare analysis of Variables in mine (variables are isolated based on setting the variable that beat SBSAT according to Anne’s result)
1 / 2
3 / 2
15 / 3
7 / 2
19 / 4
20 / 6 / X
12 / 2
14 / 3 / X
26 / 2
18 / 4
30 / 3
31 / 3
13 / 2 / X
27 / 2
32 / 2
2 / 2
6
17 / 3
21 / 3
4
5
9 / 2
16 / 3
23 / 3
10 / 2
25 / 3
28 / 2
11 / 2 / X
22 / 2
29 / 3
32
35
33
36
34
37
24
38
25
-Next step: look at these variables (from anne’s which beat SBSAT) and look at the lines that they are in and analyze the results based on that
TABLES:
Minimum: (Only appeared once)
VariableLine 28: add_state2(11, 12, 16, 23, 27, 30) / 12 / 0.129 / 806 / 807 / 5/0 / Yes (5)
6 / 0.143 / 928 / 929 / 3/0 / Yes (3)
4 / 0.129 / 775 / 776 / 3/0 / Yes (3)
5 / 0.129 / 775 / 776 / 3/0 / Yes (3)
32 / 0.127 / 840 / 841 / 4/0 / Yes (4)
33 / 0.158 / 809 / 810 / 3/0 / Yes (3)
36 / 0.158 / 809 / 810 / 3/0 / Yes (3)
34 / 0.142 / 767 / 768 / 4/0 / Yes (4)
37 / 0.142 / 767 / 768 / 4/0 / Yes (4)
38 / 0.144 / 782 / 783 / 3/0 / Yes (3)
Line 21: add_state2(9, 10, 14, 21, 25, 28) / 25 / 0.130 / 856 / 857 / 6/0 / Yes (6)
Maximum:
Variable: 20 / Number Times: 6Line 12: add_state2(1, 2, 6, 13, 17, 20) / 0.143 / 928 / 929 / 3/0 / Yes (3)
0.129 / 775 / 776 / 3/0 / Yes (3)
0.152 / 766 / 767 / 3/0 / Yes (3)
0.144 / 782 / 783 / 3/0 / Yes (3)
0.152 / 766 / 767 / 3/0 / Yes (3)
Note: all produced the same amount of solutions
Possible things to do:
-combination of commenting and un-commenting unusual result lines
Analysis Steps:
1.)unusual results (#choicepoints (small or big), # solutions (big))
2.)variables in unusual results
3.)amount of variables
4.)look at least number of times variable appears (blue) and maximum times (red)
5.)look at choice points and backtracks (data corresponding to those variables in the first lines)
6.)eliminate clauses on the lines, see which is part of core
7.)eliminate variables using exist to see if part of core
Errors:
-counting number of times variable appears (need to double check)
Consolidated:
AnneLine 28: add_state2(11, 12, 16, 23, 27, 30) / 12 / 0.129 / 806 / 807 / 5/0 / Yes (5) / +11, +13, +/-12
-11, +25, +/-12
Line 21: add_state2(9, 10, 14, 21, 25, 28) / 25 / 0.130 / 856 / 857 / 6/0 / Yes (6) / -11, +/- 25, +/-9
-11, +25, +/-12
Line 12: add_state2(1, 2, 6, 13, 17, 20) / 20 / 0.143 / 928 / 929 / 3/0 / Yes (3) / Set one variable, choosing 20 beat SBSAT
+20,
& +/-
8
17
27
29
30
31
Position of variable: no pattern
Anne’s Commandline Argument:
./sbsat slider_40_sat.ite --break-xors 0 -L 0 -All 0 --max-solutions 0 --preset-variables “Var #”
To do: Rerun the ones that im confused on (check where error is)
Anne:
From equation
-Found that position of variable produces 0 choicepoints (automatically unsatisfiable) for both sliders
-The sign of the variable is important (+, ***- , -)
Variable / Result12 / Barely Lost to SBSAT (3 choicepoints)
6 / Lost
4 / Lost Badly
5 / Lost Badly (not as badly as 4)
32 / Lost (not as badly as 4 & 5, about 100 choice points)
33 / Lost (like 32)
36 / Lost Badly
34 / Lost (like 32)
37 / Died (1118)
38 / Lost Badly
25 / Barely Lost
20 / Beat it by 1
Anne’s Result based on Setting One variable:
Similar result!
Look at steps.