Skip to content

Commit

Permalink
first commit
Browse files Browse the repository at this point in the history
  • Loading branch information
@ashukla411
ashukla411 committed Nov 3, 2018
0 parents commit 018e139
Show file tree
Hide file tree
Showing 24 changed files with 6,088 additions and 0 deletions.
Binary file added ass1/assn1.pdf
Binary file not shown.
Binary file added ass1/files/4418_1.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_2.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_3.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_4.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_5.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_6.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/4418_7.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ass1/files/REPORT.docx
Binary file not shown.
Binary file added ass1/files/assn1.pdf
Binary file not shown.
1,502 changes: 1,502 additions & 0 deletions ass1/files/file.cnf

Large diffs are not rendered by default.

2,224 changes: 2,224 additions & 0 deletions ass1/files/file1.cnf

Large diffs are not rendered by default.

2,002 changes: 2,002 additions & 0 deletions ass1/files/file2.cnf

Large diffs are not rendered by default.

28 changes: 28 additions & 0 deletions ass1/files/generate.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#!/usr/bin/python
import random

#ran on cse machine under z5151301

variables = input("Enter the number of propositional variables:\n")
clauses = input("Enter the number of clauses to generate randomly:\n")
#creating only 1 file.cnf to test, so run the entire program multiple times to test different scenarios
file=open("file.cnf","wb")
file.write("c example CNF file with {} propositional variables and {} clauses\n".format(variables,clauses))
file.write("p cnf {} {}\n".format(variables,clauses))

#generating random clauses and variable formulas in those clauses
for i in range(1,clauses+1):
formula = ""
j=0
#4 literal specification for 4-SAT
while(j<4):
num = random.randint(-variables,variables)
while(num==0):
num = random.randint(-variables,variables)
if (`num` not in formula and `-num` not in formula):
formula = formula + `num` +" "
j=j+1
formula = formula+"0\n"
#writing a clause into a file-line for 4-SAT only
file.write(formula)
file.close()
53 changes: 53 additions & 0 deletions ass1/files/out.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 150 |
| Number of clauses: 1500 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 150 1500 6000 | 550 100 20 | 0.004 % |
| 250 | 150 1500 6000 | 605 250 22 | 0.004 % |
| 475 | 150 1500 6000 | 665 475 22 | 0.004 % |
| 812 | 150 1500 6000 | 732 466 19 | 0.004 % |
| 1318 | 150 1500 6000 | 805 593 18 | 0.004 % |
| 2077 | 150 1500 6000 | 885 507 17 | 0.004 % |
| 3216 | 150 1500 6000 | 974 724 17 | 0.004 % |
| 4924 | 150 1500 6000 | 1071 928 18 | 0.004 % |
| 7486 | 150 1500 6000 | 1178 747 16 | 0.004 % |
| 11330 | 150 1500 6000 | 1296 999 17 | 0.004 % |
| 17096 | 150 1500 6000 | 1426 819 17 | 0.004 % |
| 25745 | 150 1500 6000 | 1569 745 17 | 0.004 % |
| 38719 | 150 1500 6000 | 1726 950 17 | 0.004 % |
| 58180 | 150 1500 6000 | 1898 1140 19 | 0.004 % |
| 87372 | 150 1500 6000 | 2088 1415 18 | 0.004 % |
| 131161 | 150 1500 6000 | 2297 1786 18 | 0.004 % |
| 196845 | 150 1500 6000 | 2527 2280 19 | 0.004 % |
| 295371 | 150 1500 6000 | 2779 2266 18 | 0.004 % |
| 443160 | 150 1500 6000 | 3057 2515 18 | 0.004 % |
| 664843 | 150 1500 6000 | 3363 1790 19 | 0.004 % |
| 997368 | 150 1500 6000 | 3700 3317 18 | 0.004 % |
| 1496156 | 150 1500 6000 | 4070 2000 19 | 0.004 % |
| 2244338 | 150 1500 6000 | 4477 3681 19 | 0.004 % |
| 3366612 | 150 1500 6000 | 4924 3282 19 | 0.004 % |
| 5050023 | 150 1500 6000 | 5417 4370 17 | 0.004 % |
| 7575139 | 150 1500 6000 | 5959 4126 18 | 0.004 % |
| 11362814 | 150 1500 6000 | 6554 3482 17 | 0.004 % |
| 17044326 | 150 1500 6000 | 7210 4567 18 | 0.004 % |
| 25566595 | 150 1500 6000 | 7931 4383 18 | 0.004 % |
| 38349998 | 150 1500 6000 | 8724 7853 18 | 0.004 % |
| 57525103 | 150 1500 6000 | 9597 4846 17 | 0.004 % |
===============================================================================
restarts : 85432
conflicts : 65763643 (53495 /sec)
decisions : 77513578 (0.00 % random) (63053 /sec)
propagations : 1670099599 (1358538 /sec)
conflict literals : 1300132115 (17.30 % deleted)
Memory used : 12.00 MB
CPU time : 1229.34 s

INDETERMINATE
31 changes: 31 additions & 0 deletions ass1/files/out1.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 200 |
| Number of clauses: 1479 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 200 1479 5916 | 542 100 31 | 0.003 % |
| 250 | 200 1479 5916 | 596 250 29 | 0.003 % |
| 475 | 200 1479 5916 | 656 475 28 | 0.003 % |
| 812 | 200 1479 5916 | 721 445 26 | 0.003 % |
| 1318 | 200 1479 5916 | 793 571 26 | 0.003 % |
| 2077 | 200 1479 5916 | 873 495 24 | 0.003 % |
| 3216 | 200 1479 5916 | 960 713 26 | 0.003 % |
| 4924 | 200 1479 5916 | 1056 909 24 | 0.003 % |
| 7486 | 200 1479 5916 | 1162 700 25 | 0.003 % |
===============================================================================
restarts : 34
conflicts : 8307 (98893 /sec)
decisions : 11255 (0.00 % random) (133988 /sec)
propagations : 283551 (3375607 /sec)
conflict literals : 243567 (11.65 % deleted)
Memory used : 5.00 MB
CPU time : 0.084 s

SATISFIABLE
37 changes: 37 additions & 0 deletions ass1/files/out2.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 100 |
| Number of clauses: 1473 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 100 1473 5892 | 540 100 13 | 0.010 % |
| 250 | 100 1473 5892 | 594 250 13 | 0.010 % |
| 475 | 100 1473 5892 | 653 475 12 | 0.010 % |
| 812 | 100 1473 5892 | 718 475 12 | 0.010 % |
| 1318 | 100 1473 5892 | 790 617 12 | 0.010 % |
| 2077 | 100 1473 5892 | 869 574 10 | 0.010 % |
| 3216 | 100 1473 5892 | 956 838 11 | 0.010 % |
| 4924 | 100 1473 5892 | 1052 600 10 | 0.010 % |
| 7486 | 100 1473 5892 | 1157 1036 11 | 0.010 % |
| 11330 | 100 1473 5892 | 1273 783 10 | 0.010 % |
| 17096 | 100 1473 5892 | 1400 770 10 | 0.010 % |
| 25745 | 100 1473 5892 | 1540 965 11 | 0.010 % |
| 38719 | 100 1473 5892 | 1695 1522 10 | 0.010 % |
| 58180 | 100 1473 5892 | 1864 1364 11 | 0.010 % |
| 87372 | 100 1473 5892 | 2051 1461 9 | 0.020 % |
===============================================================================
restarts : 284
conflicts : 107873 (108306 /sec)
decisions : 124131 (0.00 % random) (124630 /sec)
propagations : 1845984 (1853398 /sec)
conflict literals : 1159895 (21.09 % deleted)
Memory used : 5.00 MB
CPU time : 0.996 s

UNSATISFIABLE
23 changes: 23 additions & 0 deletions ass1/files/out3.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 50 |
| Number of clauses: 1450 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 49 1450 5800 | 531 99 5 | 2.080 % |
===============================================================================
restarts : 2
conflicts : 198 (inf /sec)
decisions : 213 (0.00 % random) (inf /sec)
propagations : 1630 (inf /sec)
conflict literals : 856 (22.32 % deleted)
Memory used : 5.00 MB
CPU time : 0 s

UNSATISFIABLE
23 changes: 23 additions & 0 deletions ass1/files/out4.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 30 |
| Number of clauses: 464 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 28 463 1852 | 169 98 5 | 7.004 % |
===============================================================================
restarts : 2
conflicts : 125 (inf /sec)
decisions : 138 (0.00 % random) (inf /sec)
propagations : 920 (inf /sec)
conflict literals : 517 (21.19 % deleted)
Memory used : 5.00 MB
CPU time : 0 s

UNSATISFIABLE
23 changes: 23 additions & 0 deletions ass1/files/out5.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 150 |
| Number of clauses: 150 |
| Parse time: 0.00 s |
| Eliminated clauses: 0.00 Mb |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
===============================================================================
restarts : 1
conflicts : 0 (-nan /sec)
decisions : 1 (0.00 % random) (inf /sec)
propagations : 0 (-nan /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 5.00 MB
CPU time : 0 s

SATISFIABLE
23 changes: 23 additions & 0 deletions ass1/files/out6.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 1486 |
| Number of clauses: 150 |
| Parse time: 0.00 s |
| Eliminated clauses: 0.01 Mb |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
===============================================================================
restarts : 1
conflicts : 0 (-nan /sec)
decisions : 1 (0.00 % random) (inf /sec)
propagations : 0 (-nan /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 5.00 MB
CPU time : 0 s

SATISFIABLE
23 changes: 23 additions & 0 deletions ass1/files/out7.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 1999 |
| Number of clauses: 200 |
| Parse time: 0.00 s |
| Eliminated clauses: 0.02 Mb |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
===============================================================================
restarts : 1
conflicts : 0 (-nan /sec)
decisions : 1 (0.00 % random) (inf /sec)
propagations : 0 (-nan /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 5.00 MB
CPU time : 0 s

SATISFIABLE
46 changes: 46 additions & 0 deletions ass1/files/out8.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 150 |
| Number of clauses: 1400 |
| Parse time: 0.00 s |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
| 100 | 150 1400 5600 | 513 100 22 | 0.004 % |
| 250 | 150 1400 5600 | 564 250 22 | 0.004 % |
| 475 | 150 1400 5600 | 621 475 22 | 0.004 % |
| 812 | 150 1400 5600 | 683 487 20 | 0.004 % |
| 1318 | 150 1400 5600 | 751 633 18 | 0.004 % |
| 2077 | 150 1400 5600 | 826 608 18 | 0.004 % |
| 3216 | 150 1400 5600 | 909 463 17 | 0.004 % |
| 4924 | 150 1400 5600 | 1000 774 18 | 0.004 % |
| 7486 | 150 1400 5600 | 1100 764 17 | 0.004 % |
| 11330 | 150 1400 5600 | 1210 661 18 | 0.004 % |
| 17096 | 150 1400 5600 | 1331 840 18 | 0.004 % |
| 25745 | 150 1400 5600 | 1464 1334 20 | 0.004 % |
| 38719 | 150 1400 5600 | 1611 873 18 | 0.004 % |
| 58180 | 150 1400 5600 | 1772 1484 19 | 0.004 % |
| 87372 | 150 1400 5600 | 1949 959 18 | 0.004 % |
| 131161 | 150 1400 5600 | 2144 1209 19 | 0.004 % |
| 196845 | 150 1400 5600 | 2358 1625 19 | 0.004 % |
| 295371 | 150 1400 5600 | 2594 2135 20 | 0.004 % |
| 443160 | 150 1400 5600 | 2854 1430 19 | 0.004 % |
| 664843 | 150 1400 5600 | 3139 2265 20 | 0.004 % |
| 997368 | 150 1400 5600 | 3453 1655 17 | 0.004 % |
| 1496156 | 150 1400 5600 | 3798 2056 20 | 0.004 % |
| 2244338 | 150 1400 5600 | 4178 3095 19 | 0.004 % |
| 3366612 | 150 1400 5600 | 4596 2947 20 | 0.004 % |
===============================================================================
restarts : 7676
conflicts : 4331290 (72439 /sec)
decisions : 5191849 (0.00 % random) (86832 /sec)
propagations : 113728245 (1902065 /sec)
conflict literals : 90315255 (15.31 % deleted)
Memory used : 5.00 MB
CPU time : 59.792 s

SATISFIABLE
Loading

0 comments on commit 018e139

Please sign in to comment.