CNF is clausal normal form
can express any concievable probositional statement
nish negation
c nish ANDNOT nish 0101.ena0101 du 0000 no to all (nothing)
p cnf 1 2
1 0
-1 0
c nish ORNOT nish 0101.ana0101 du 1111 yes to all (everything)
p cnf 1 1
1 -1 0
nish relationship loki
c nish AND loki 0101 .e 0011 du 0001
p cnf 2 2
1 0
2 0
c nish NOR loki ( NOTORNOT ) 0101nai.ana0011 du 1110
p cnf 2 1
-1 -2 0
c nish NOTAND loki 0101 nai.e 0011 du 0010
p cnf 2 2
-1 0
2 0
c nish IMPLIES ( ORNOT ) loki 0101 .ana 0011 du 1101
p cnf 2 1
1 -2 0
c nish ORANDNOTOR loki 0101.a0011.e0101nai.a0011 du 0011 OR AND NOT OR
p cnf 2 2
1 2 0
-1 2 0
c nish ORNOTANDNOTORNOT loki 0101.ana0011.e0101nai.ana0011 du 1100 OR NOT AND NOT OR NOT
p cnf 2 2
1 -2 0
-1 -2 0
c nish ANDNOT loki 0101 .ena 0011 du 0100 AND NOT
p cnf 2 2
1 0
-2 0
c nish THERFORE ( NOTOR ) loki 0101 nai.a 0011 du 1011 THERFORE NOT OR
p cnf 2 1
-1 2 0
c nish XOR loki (ORANDNOTORNOT) 0101.a0011.e0101nai.ana0011 du 0110 XOR OR AND NOT OR NOT
p cnf 2 2
1 2 0
-1 -2 0
c nish IFF ( ORNOTANDNOTOR ) loki 0101.ana0011.e0101nai.a0011 du 1001
p cnf 2 2
1 -2 0
-1 2 0
c nish NAND loki (NOTANDNOT) 0101nai.ena0011 du 1000
p cnf 2 2
-1 0
-2 0
c nish OR loki 0101 .a 0011 du 0111
p cnf 2 1
1 2 0
c nish ANDORNOT loki 0101.a0011.e0101.ana0011 du 0101 OR AND OR NOT
p cnf 2 2
1 2 0
1 -2 0
c nish NOTORANDNOTORNOT loki 0101nai.a0011.e0101nai.ana0011du 1010 NOT OR AND NOT OR NOT
p cnf 2 2
-1 2 0
1 -2 0
loki@rurix 22:11:36 ~/skamSELypla/sat $ ./configure
Configuring sat-1.0...
configure: Dependency base-any: using base-1.0
configure: Using install prefix: /usr/local
configure: Binaries installed in: /usr/local/bin
configure: Libraries installed in: /usr/local/lib/sat-1.0/ghc-6.4.2
configure: Private binaries installed in: /usr/local/libexec
configure: Data files installed in: /usr/local/share/sat-1.0
configure: Using compiler: /usr/bin/ghc
configure: Compiler flavor: GHC
configure: Compiler version: 6.4.2
configure: Using package tool: /usr/bin/ghc-pkg
configure: Using ar found on system at: /usr/bin/ar
configure: Using haddock found on system at: /usr/bin/haddock
configure: No pfesetup found
configure: Using ranlib found on system at: /usr/bin/ranlib
configure: Using runghc found on system at: /usr/bin/runghc
configure: No runhugs found
configure: No happy found
configure: No alex found
configure: Using hsc2hs: /usr/bin/hsc2hs
configure: No c2hs found
configure: No cpphs found
configure: No greencard found
loki@rurix 22:11:49 ~/skamSELypla/sat $ make
Preprocessing executables for sat-1.0...
Building sat-1.0...
Chasing modules from: SATSolver.hs
Skipping Main ( SATSolver.hs, dist/build/SATSolve/SATSolve-tmp/Main.o )
dist/build/SATSolve/SATSolve is up to date, linking not required.
Chasing modules from: CNFGenerator.hs
Skipping Main ( CNFGenerator.hs, dist/build/CNFGenerate/CNFGenerate-tmp/Main.o )
dist/build/CNFGenerate/CNFGenerate is up to date, linking not required.
loki@rurix 22:11:52 ~/skamSELypla/sat $ dist/build/CNFGenerate/CNFGenerate --help
$ SATGenerate <# of variables> <# of clauses> <# of variables per clause> >
loki@rurix 22:16:26 ~/skamSELypla/sat $ dist/build/CNFGenerate/CNFGenerate 15 30 3 > test.cnf
#################################################################################################################################
# all example problem sets are 3-CNF which have a clausal length of three,
# 3-CNF is considerd the hardest concievable class of problems
# They are NP-Complete out of NP-Hard problems
#################################################################################################################################
Version 1.0
loki@rurix 22:16:30 ~/skamSELypla/sat $ dist/build/SATSolve/SATSolve test.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 15 30
number of variables: 15 hex: f
number of clauses: 30 hex: 1e
max variable combinations:32768 hex: 8000
number of atempts: 89 hex: 59
assignment of variables: [0,0,0,0,0,1,0,1,0,1,1,1,1,0,0]
CNF evaluation result: 1
loki@rurix 22:16:34 ~/skamSELypla/sat $ time dist/build/SATSolve/SATSolve test.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 15 30
number of variables: 15 hex: f
number of clauses: 30 hex: 1e
max variable combinations:32768 hex: 8000
number of atempts: 22 hex: 16
assignment of variables: [0,0,1,1,0,1,1,0,1,0,0,1,0,1,1]
CNF evaluation result: 1
real 0m0.010s
user 0m0.004s
sys 0m0.004s
loki@rurix 22:16:41 ~/skamSELypla/sat $ time dist/build/CNFGenerate/CNFGenerate 30 90 3 > test.cnf
real 0m0.007s
user 0m0.000s
sys 0m0.004s
loki@rurix 22:17:04 ~/skamSELypla/sat $ time dist/build/SATSolve/SATSolve test.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 30 90
number of variables: 30 hex: 1e
number of clauses: 90 hex: 5a
max variable combinations:1073741824 hex: 40000000
number of atempts: 37276 hex: 919c
assignment of variables: [1,1,1,1,1,0,0,1,0,1,1,0,1,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0]
CNF evaluation result: 1
real 0m2.026s
user 0m1.932s
sys 0m0.008s
loki@rurix 22:17:12 ~/skamSELypla/sat $
Version 1.1:
loki@rurix 14:59:31 ~/CKUle/cse4401 $ CNFGenerate 50 50 3 > prob1.cnf
loki@rurix 14:59:36 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 50 50
number of variables: 50 hex: 32
number of clauses: 50 hex: 32
max variable combinations:1125899906842624 hex: 4000000000000
number of atempts: 1 hex: 1
assignment of variables: [1,1,0,1,1,1,1,0,1,1,0,0,1,0,1,1,1,0,0,0,1,0,0,1,1,1,0,1,1,0,0,1,0,1,0,1,0,1,1,1,0,0,0,1,0,1,0,1,1,0]
number of clauses solved: 46 hex: 2e
number of atempts: 13 hex: d
assignment of variables: [0,1,1,1,1,1,1,1,1,1,1,0,1,0,0,1,1,0,1,0,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,0,1,1,0,1,1,0,0,1,1,1,0]
number of clauses solved: 47 hex: 2f
number of atempts: 21 hex: 15
assignment of variables: [1,1,1,1,1,1,0,0,0,0,0,1,1,0,1,0,1,1,1,1,0,0,0,1,0,1,0,0,1,0,1,1,1,0,1,1,1,1,1,0,1,1,1,0,0,1,1,0,1,0]
number of clauses solved: 48 hex: 30
number of atempts: 118 hex: 76
assignment of variables: [0,1,0,1,0,0,1,0,0,1,1,0,1,1,0,1,1,1,0,0,1,0,1,0,0,1,1,0,0,1,1,0,0,1,1,1,0,1,1,1,1,1,1,0,1,1,1,1,1,0]
number of clauses solved: 49 hex: 31
number of atempts: 336 hex: 150
assignment of variables: [1,1,0,0,1,1,1,0,0,1,0,0,1,0,1,0,0,1,0,0,0,1,0,1,1,0,0,1,1,1,0,1,0,1,0,0,0,0,1,1,0,0,1,1,0,0,1,1,1,1]
number of clauses solved: 50
SATisfiable
real 0m0.075s
user 0m0.068s
sys 0m0.004s
loki@rurix 14:59:39 ~/CKUle/cse4401 $ CNFGenerate 50 100 3 > prob1.cnf
loki@rurix 14:59:57 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 50 100
number of variables: 50 hex: 32
number of clauses: 100 hex: 64
max variable combinations:1125899906842624 hex: 4000000000000
number of atempts: 1 hex: 1
assignment of variables: [0,0,0,0,0,0,0,0,0,1,1,0,1,1,1,1,0,0,0,0,0,0,1,1,0,1,1,0,1,0,1,0,1,1,1,0,0,0,0,0,0,1,0,1,0,1,1,0,1,0]
number of clauses solved: 90 hex: 5a
number of atempts: 7 hex: 7
assignment of variables: [0,0,1,1,1,0,1,0,0,0,0,1,0,1,0,1,0,1,0,0,0,0,0,0,0,0,0,1,0,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,1,0,0,0,0]
number of clauses solved: 92 hex: 5c
number of atempts: 11 hex: b
assignment of variables: [0,1,0,1,0,1,0,1,1,0,1,0,0,1,0,0,1,0,1,0,1,0,0,0,0,0,1,1,1,1,1,1,1,0,0,0,0,1,0,1,0,0,1,0,0,0,1,1,0,0]
number of clauses solved: 93 hex: 5d
number of atempts: 60 hex: 3c
assignment of variables: [0,0,1,0,1,0,0,0,1,0,1,1,1,1,0,1,1,1,0,1,1,0,1,1,0,0,0,1,0,0,0,0,0,1,0,0,1,0,1,0,0,1,1,0,0,0,0,0,1,0]
number of clauses solved: 94 hex: 5e
number of atempts: 133 hex: 85
assignment of variables: [0,0,1,0,0,0,1,1,1,1,0,1,0,1,1,1,1,0,1,1,1,0,1,0,0,0,0,0,1,0,1,1,0,1,1,0,1,1,0,0,0,1,1,1,0,1,0,1,1,1]
number of clauses solved: 96 hex: 60
number of atempts: 140 hex: 8c
assignment of variables: [0,0,0,1,1,1,0,0,0,0,1,1,1,1,1,1,1,1,0,0,1,0,0,0,0,1,0,1,0,1,0,1,0,1,1,0,0,0,1,0,0,1,0,1,0,1,1,1,1,1]
number of clauses solved: 98 hex: 62
number of atempts: 7023 hex: 1b6f
assignment of variables: [0,0,1,0,1,1,0,1,1,0,1,1,0,1,1,1,1,1,1,1,1,1,1,1,0,1,0,1,1,0,1,1,0,0,0,0,0,1,0,1,1,1,1,1,0,1,1,0,1,1]
number of clauses solved: 99 hex: 63
number of atempts: 97320 hex: 17c28
assignment of variables: [0,1,1,0,0,1,0,1,0,0,1,0,0,1,0,1,1,1,0,1,0,0,1,0,0,1,1,1,0,1,1,1,0,0,0,1,0,1,0,1,1,1,1,0,0,1,0,0,1,0]
number of clauses solved: 100
SATisfiable
real 0m24.505s
user 0m24.406s
sys 0m0.056s
loki@rurix 15:00:25 ~/CKUle/cse4401 $ CNFGenerate 50 200 3 > prob1.cnf
loki@rurix 15:00:47 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 50 200
number of variables: 50 hex: 32
number of clauses: 200 hex: c8
max variable combinations:1125899906842624 hex: 4000000000000
number of atempts: 1 hex: 1
assignment of variables: [0,1,0,1,0,0,1,1,1,1,0,1,0,0,1,1,1,1,1,0,0,1,1,1,0,0,0,0,1,1,1,1,1,1,0,1,1,0,1,0,1,1,0,1,1,1,1,0,1,0]
number of clauses solved: 175 hex: af
number of atempts: 4 hex: 4
assignment of variables: [1,1,0,0,0,1,0,1,0,1,1,1,1,0,1,0,0,1,0,1,0,0,1,0,1,0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1]
number of clauses solved: 179 hex: b3
number of atempts: 10 hex: a
assignment of variables: [0,0,0,0,1,0,1,1,0,1,0,1,1,0,1,0,0,0,0,0,0,1,0,1,1,0,1,1,1,0,1,1,0,0,1,0,1,0,0,1,0,1,0,1,1,1,1,0,1,0]
number of clauses solved: 182 hex: b6
number of atempts: 29 hex: 1d
assignment of variables: [1,0,0,1,0,0,0,1,1,0,1,1,0,0,1,1,1,1,0,1,0,1,1,1,1,0,1,1,1,0,1,1,1,0,1,1,1,1,0,1,1,0,0,0,1,1,0,1,0,0]
number of clauses solved: 183 hex: b7
number of atempts: 116 hex: 74
assignment of variables: [1,1,1,1,0,0,0,0,0,1,1,1,0,1,0,1,0,0,1,0,1,1,0,0,1,1,1,1,1,1,0,1,1,0,0,0,0,1,0,0,0,0,1,0,0,1,1,1,1,0]
number of clauses solved: 184 hex: b8
number of atempts: 195 hex: c3
assignment of variables: [1,0,1,0,0,1,0,1,1,1,0,1,0,1,0,0,1,1,0,1,1,1,1,1,0,0,0,1,1,0,0,1,0,0,1,1,1,1,0,0,1,0,1,0,1,0,0,1,0,0]
number of clauses solved: 185 hex: b9
number of atempts: 251 hex: fb
assignment of variables: [0,0,1,1,1,0,1,1,1,0,0,0,0,0,1,1,0,0,1,0,1,1,1,1,0,1,0,0,0,1,0,1,0,0,1,0,1,1,1,0,1,1,1,0,1,0,0,1,0,0]
number of clauses solved: 188 hex: bc
number of atempts: 1152 hex: 480
assignment of variables: [0,0,1,1,1,0,1,0,0,1,0,0,0,0,1,0,0,1,0,1,1,0,0,0,0,0,1,1,1,1,1,0,1,0,0,1,1,0,0,0,1,0,0,1,0,0,0,1,0,0]
number of clauses solved: 189 hex: bd
number of atempts: 2383 hex: 94f
assignment of variables: [0,1,0,0,0,0,0,1,0,0,1,1,0,1,0,1,0,0,0,1,0,0,1,1,0,1,0,1,1,1,1,1,0,0,1,0,1,0,1,0,0,0,1,1,1,0,0,0,0,1]
number of clauses solved: 190 hex: be
number of atempts: 17386 hex: 43ea
assignment of variables: [0,0,1,1,1,0,0,1,0,1,1,1,1,0,1,0,1,1,0,0,0,1,1,1,0,0,0,0,0,0,1,1,0,0,0,0,1,1,0,1,0,0,0,1,1,0,0,0,0,0]
number of clauses solved: 191 hex: bf
number of atempts: 29468 hex: 731c
assignment of variables: [1,0,0,0,1,0,0,1,0,0,1,0,0,0,0,0,1,1,0,1,0,0,1,1,0,0,0,1,0,1,1,1,1,0,1,0,0,1,0,1,1,1,1,0,0,0,0,0,0,0]
number of clauses solved: 193 hex: c1
SATSolve: interrupted
real 1m34.460s
user 1m7.692s
sys 0m0.172s
loki@rurix 15:02:24 ~/CKUle/cse4401 $
loki@rurix 15:02:24 ~/CKUle/cse4401 $ CNFGenerate 100 350 3 > prob1.cnf
loki@rurix 15:06:21 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 100 350
number of variables: 100 hex: 64
number of clauses: 350 hex: 15e
max variable combinations:1267650600228229401496703205376 hex: 10000000000000000000000000
number of atempts: 1 hex: 1
assignment of variables: [1,1,1,1,1,0,1,1,1,0,1,1,1,1,0,1,0,1,0,0,0,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,0,1,0,0,0,1,0,0,0,0,1,0,0,0,1,0,1,1,1,1,1,1,1,0,1,0,1,1,0,0,0,1,0,1,1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,1,1,0,1,0,0,0,0,1,1,1,1,1,1,1]
number of clauses solved: 308 hex: 134
number of atempts: 3 hex: 3
assignment of variables: [1,0,0,0,0,0,1,0,0,0,0,1,1,0,0,0,1,1,0,1,1,0,0,1,0,1,0,0,1,1,1,1,0,0,0,0,1,1,0,0,0,0,1,1,1,0,0,0,0,1,1,1,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,0,0,1,1,1,1,0,0,0,0,1,1,0,1,0,0,0,0,0,0,0,0,1,0,0,1,0,0,0,0]
number of clauses solved: 313 hex: 139
number of atempts: 18 hex: 12
assignment of variables: [0,0,0,0,1,0,0,1,0,0,0,1,1,1,1,0,0,1,0,1,1,1,0,0,0,1,0,1,0,1,0,0,1,0,1,1,1,0,0,1,1,1,1,0,1,0,1,0,1,0,0,1,1,0,0,0,1,0,1,1,0,0,1,1,0,0,0,1,0,0,1,1,1,0,0,0,0,0,0,1,0,1,0,1,1,0,0,1,0,1,0,1,0,0,0,1,0,0,1,1]
number of clauses solved: 314 hex: 13a
number of atempts: 21 hex: 15
assignment of variables: [1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,0,1,0,1,1,1,0,0,0,1,0,0,0,0,0,1,0,0,0,1,1,1,1,1,1,0,1,0,1,0,0,1,0,0,0,0,1,0,1,1,0,1,1,1,0,1,0,1,1,0,1,1,1,0,0,1,0,1,0,1,0,0,1,0,1,0,1,1,1,1,1,1,1,1,0,1,1,0,1,1,1,1,0,1]
number of clauses solved: 319 hex: 13f
number of atempts: 91 hex: 5b
assignment of variables: [1,1,0,1,1,0,0,0,0,1,1,1,1,1,0,0,1,1,1,1,0,0,0,1,0,0,1,0,1,0,0,0,0,0,0,0,0,1,0,1,1,1,0,0,1,0,1,1,1,1,1,0,1,0,0,0,1,1,1,1,0,0,0,1,1,0,0,0,0,0,1,0,0,1,0,0,0,1,1,0,0,1,1,1,1,0,1,1,1,0,1,1,0,0,0,1,1,0,0,1]
number of clauses solved: 320 hex: 140
number of atempts: 156 hex: 9c
assignment of variables: [1,1,1,0,0,0,0,1,0,0,0,0,1,1,0,1,1,0,1,1,0,0,1,1,1,1,1,0,1,1,0,0,0,1,0,1,0,0,1,1,0,0,1,0,1,1,1,1,0,0,0,1,0,0,0,1,1,1,1,0,0,1,1,0,1,0,0,1,0,1,0,1,0,1,1,0,0,1,0,1,1,1,0,1,0,0,0,1,0,0,0,1,1,1,0,0,1,0,1,0]
number of clauses solved: 321 hex: 141
number of atempts: 192 hex: c0
assignment of variables: [1,1,1,0,1,0,0,1,1,0,0,0,0,0,1,0,0,0,1,1,1,0,0,0,0,0,0,0,1,0,1,0,1,0,1,1,1,1,0,1,1,1,1,0,1,0,0,0,1,1,0,0,0,0,1,0,0,1,1,0,1,0,0,0,0,0,0,0,1,0,1,0,0,1,0,1,1,1,0,0,0,0,0,1,1,0,1,1,0,0,0,1,0,0,0,1,0,0,1,0]
number of clauses solved: 323 hex: 143
number of atempts: 379 hex: 17b
assignment of variables: [0,0,0,0,0,1,1,1,0,0,1,1,1,1,0,0,1,0,0,0,1,1,0,0,0,1,0,1,0,1,1,0,0,0,1,0,1,0,0,1,1,0,1,1,0,1,1,1,0,0,1,0,0,1,0,1,0,1,0,0,0,1,1,1,0,0,0,0,0,0,0,1,0,0,1,0,0,1,0,0,1,0,1,0,0,0,0,1,0,1,1,1,0,1,0,0,1,0,1,0]
number of clauses solved: 324 hex: 144
number of atempts: 588 hex: 24c
assignment of variables: [1,1,0,0,1,0,1,0,0,1,1,1,0,1,1,1,0,1,1,1,0,1,1,0,0,0,0,1,1,1,1,0,0,0,1,0,1,0,1,0,1,0,0,1,1,1,1,0,0,1,1,1,1,0,1,0,1,1,1,1,0,1,0,0,0,1,0,1,1,0,0,1,0,0,1,0,0,0,1,1,0,0,0,1,0,0,1,1,1,0,0,1,0,0,0,1,0,1,0,1]
number of clauses solved: 325 hex: 145
number of atempts: 2811 hex: afb
assignment of variables: [1,0,0,0,0,0,1,1,0,0,0,0,1,1,0,1,1,1,1,0,1,1,0,1,1,1,0,1,1,1,0,0,0,1,1,0,1,1,0,1,0,0,0,1,1,0,1,0,0,1,0,1,1,0,1,1,0,1,0,0,1,1,1,0,0,1,1,0,1,1,1,1,0,0,0,0,0,1,1,1,1,0,0,1,1,0,1,0,1,0,0,0,1,0,0,1,0,1,0,1]
number of clauses solved: 326 hex: 146
number of atempts: 4395 hex: 112b
assignment of variables: [0,1,0,0,0,0,1,0,0,1,0,0,1,1,0,1,0,1,1,0,1,1,0,1,0,1,0,0,0,0,0,1,1,0,1,1,1,1,0,1,1,1,0,1,1,1,0,1,0,0,1,0,1,1,1,1,1,0,1,1,0,0,0,0,1,0,1,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,1,1,1,0,0,1,1,0,0,1,1,1,0,1,0,1,1,1]
number of clauses solved: 329 hex: 149
number of atempts: 20591 hex: 506f
assignment of variables: [0,0,0,1,0,0,1,1,0,1,1,0,1,1,0,1,1,1,1,0,0,0,1,0,0,1,0,0,1,1,0,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,0,1,0,0,0,1,0,0,1,0,0,0,1,0,1,0,0,0,0,1,1,1,1,0,1,0,0,1,0,0,0,0,1,0,0,0,1,1,1,0,1,0,0,0,0,1,0,0,0,1,1,0,0,0]
number of clauses solved: 330 hex: 14a
number of atempts: 22961 hex: 59b1
assignment of variables: [1,0,0,1,1,0,1,0,0,0,1,0,0,0,1,1,0,0,0,0,0,1,1,1,1,0,0,1,1,1,1,1,0,0,0,0,1,0,0,0,1,1,1,0,1,0,1,0,1,0,0,1,0,0,0,0,0,1,0,1,0,1,0,1,1,0,0,1,1,0,1,1,0,1,1,0,0,0,0,0,0,0,1,1,0,1,0,0,1,0,0,0,0,1,1,1,1,0,1,0]
number of clauses solved: 333 hex: 14d
SATSolve: interrupted
real 1m17.128s
user 1m16.281s
sys 0m0.176s
loki@rurix 15:07:43 ~/CKUle/cse4401 $
loki@rurix 15:07:43 ~/CKUle/cse4401 $ CNFGenerate 300 400 3 > prob1.cnf
loki@rurix 15:08:48 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 300 400
number of variables: 300 hex: 12c
number of clauses: 400 hex: 190
max variable combinations:2037035976334486086268445688409378161051468393665936250636140449354381299763336706183397376 hex: 1000000000000000000000000000000000000000000000000000000000000000000000000000
number of atempts: 1 hex: 1
assignment of variables: [0,0,1,0,0,1,1,0,0,0,1,1,0,1,1,1,1,0,1,1,1,1,0,1,1,1,1,0,0,1,1,1,0,0,1,0,1,1,0,1,0,1,1,1,0,1,0,0,0,1,1,0,1,0,0,1,1,0,1,1,1,0,1,0,1,1,0,0,1,1,1,1,0,1,0,0,1,0,1,1,1,0,0,1,1,0,0,0,0,1,0,0,1,1,1,0,1,0,0,1,1,0,1,1,0,1,0,0,0,1,0,0,0,1,0,1,1,1,1,0,0,1,0,0,1,1,0,1,1,0,1,1,1,0,0,0,1,0,1,1,0,0,1,1,0,0,1,0,0,1,1,0,1,0,1,0,0,0,1,0,1,1,1,1,1,0,0,1,0,1,0,0,1,0,1,1,0,0,0,0,1,0,1,1,1,0,1,1,0,1,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1,0,0,0,1,0,1,1,0,0,0,0,0,1,0,0,0,0,0,1,0,1,0,1,0,0,1,1,0,1,0,1,1,1,0,1,1,0,1,1,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,1,1,1,1,0,0,1,1,1,0,0,0,1,0,0,1,0,0,0,0,0,1,0,0,1,0,1,0,0,1,1,0,1,1,0,0,0]
number of clauses solved: 350 hex: 15e
number of atempts: 3 hex: 3
assignment of variables: [1,1,1,1,1,1,1,0,1,0,1,0,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,1,1,0,1,1,0,0,0,1,0,0,0,0,0,0,1,0,1,1,1,0,0,0,1,1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,1,0,1,1,1,1,0,1,1,1,1,0,1,1,0,1,1,1,0,1,1,0,0,0,1,0,1,1,1,0,0,1,0,1,1,1,0,0,1,0,0,1,0,1,0,1,0,0,0,0,1,0,0,1,1,0,0,0,0,1,0,1,1,1,0,0,1,0,1,1,0,1,0,0,1,0,0,1,1,1,1,1,1,0,1,1,1,0,1,1,1,1,0,1,1,0,0,0,1,1,0,0,0,1,0,0,1,0,1,1,0,1,1,1,0,0,0,0,0,1,1,1,0,1,0,0,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,1,1,1,0,1,0,0,1,0,1,1,1,0,0,0,1,0,1,0,1,1,1,1,1,0,1,0,0,0,0,0,0,1,1,0,1,0,1,0,1,0,1,0,0,1,0,0,1,1,0,0,1,0,1,1,1,1,0,1,1,0,0,0,1,0,0,0,1,1,0,0,0,1,1,0,0,0,1,0,1,0,1,0,0,1,1,1,1]
number of clauses solved: 355 hex: 163
number of atempts: 12 hex: c
assignment of variables: [1,0,1,0,0,1,1,0,0,0,0,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,1,0,1,0,1,1,0,1,1,1,0,0,0,1,1,0,1,0,1,1,0,0,1,1,0,1,0,0,1,0,1,0,0,0,0,1,0,0,0,1,0,0,0,0,1,1,1,0,0,1,0,0,1,1,1,0,0,1,1,1,1,0,0,0,0,1,0,1,0,1,0,0,0,0,0,0,0,0,0,1,1,0,1,1,1,1,0,0,1,1,1,1,0,1,0,0,1,1,0,0,0,0,0,1,0,0,1,1,1,0,0,1,1,1,1,0,1,0,1,1,0,1,1,0,0,0,1,0,0,1,1,1,1,1,0,0,1,1,0,0,1,1,1,0,1,1,1,0,1,1,1,0,0,1,0,0,1,0,1,1,0,1,0,1,0,0,1,0,1,1,0,0,0,0,0,0,1,0,1,1,1,0,0,1,0,1,1,1,1,1,1,0,1,0,1,0,0,1,0,1,0,1,0,0,1,1,1,1,1,1,1,0,0,1,1,1,1,1,1,0,0,1,0,0,0,0,0,0,1,1,1,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,1,0,1,1,1,1,1,0,0,1,0,0,1,1,1,1,0,1,0,1,1,0,0,1,1,0,1]
number of clauses solved: 361 hex: 169
number of atempts: 35 hex: 23
assignment of variables: [0,0,1,1,1,1,0,0,1,1,1,0,1,1,0,1,0,1,1,0,0,0,1,1,0,1,0,1,0,0,1,1,1,0,1,0,1,0,1,1,0,0,1,1,1,0,1,1,1,1,0,1,0,1,0,1,1,0,1,1,0,1,1,1,0,0,0,0,0,1,1,0,1,1,0,0,0,1,1,1,1,0,1,0,0,0,1,0,0,0,0,1,0,1,1,0,1,0,1,0,1,1,1,1,0,1,1,0,1,1,1,1,0,0,1,0,1,1,0,1,0,1,0,0,0,0,0,0,1,0,0,0,0,1,0,1,0,0,0,1,1,1,0,1,0,0,0,0,1,0,1,0,0,1,1,0,0,1,1,1,1,1,1,0,1,0,1,0,1,0,0,0,0,1,0,1,1,0,0,1,0,1,1,1,0,0,1,0,1,1,0,0,1,0,0,0,0,0,1,1,0,0,0,1,1,1,0,0,0,1,1,1,1,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,1,0,0,0,1,1,1,1,1,1,1,0,1,0,0,1,0,1,1,0,0,0,1,1,0,0,1,0,0,1,1,0,1,1,0,0,1,1,0,1,0,1,1,1,0,1,0,0,0,0,1,0,1,1,0,0,0,0,1,1,0,1,1,0,1,1,0,0,0,1,1]
number of clauses solved: 365 hex: 16d
number of atempts: 410 hex: 19a
assignment of variables: [1,1,1,0,0,0,0,0,1,1,1,1,1,1,0,0,0,1,1,0,1,1,1,1,1,1,0,1,0,0,1,1,0,1,0,0,0,1,1,0,1,0,0,1,1,1,1,0,0,1,1,1,0,1,1,0,1,0,0,1,0,0,1,0,1,0,1,1,0,1,1,1,1,0,0,0,1,0,0,0,1,0,1,1,1,1,1,1,0,1,1,0,1,0,1,1,1,0,1,0,1,1,1,0,0,0,1,0,0,0,0,1,1,0,0,1,0,1,1,1,1,0,1,0,0,0,0,0,0,1,1,1,1,1,0,1,0,0,1,0,1,0,0,1,0,1,1,0,0,0,1,1,0,1,1,1,1,1,1,0,1,1,0,1,0,1,1,0,0,1,0,0,0,1,0,0,1,1,1,0,1,1,1,1,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0,1,1,1,0,1,0,0,1,0,1,1,0,1,1,1,1,1,0,1,0,1,1,1,0,1,1,1,0,1,0,1,1,1,0,0,0,0,0,0,1,1,1,1,0,0,1,1,0,0,1,0,1,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,1,1,1,1,1,0,1,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0]
number of clauses solved: 378 hex: 17a
SATSolve: interrupted
real 0m56.621s
user 0m55.959s
sys 0m0.072s
loki@rurix 15:09:48 ~/CKUle/cse4401 $
loki@rurix 15:09:48 ~/CKUle/cse4401 $ CNFGenerate 400 400 3 > prob1.cnf
loki@rurix 15:10:21 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 400 400
number of variables: 400 hex: 190
number of clauses: 400 hex: 190
max variable combinations:2582249878086908589655919172003011874329705792829223512830659356540647622016841194629645353280137831435903171972747493376 hex: 10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
number of atempts: 1 hex: 1
assignment of variables: [1,0,1,1,0,1,0,0,1,0,0,0,1,1,0,0,0,0,1,0,0,0,0,0,1,0,0,1,1,1,0,0,1,1,1,0,1,1,0,0,0,1,1,1,1,0,0,0,0,0,0,1,0,0,0,1,1,0,1,0,1,0,0,1,1,1,0,1,1,0,1,0,1,0,0,0,1,0,1,1,0,0,0,0,0,0,1,0,1,1,1,0,1,1,0,1,1,0,0,1,1,0,0,1,1,1,0,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,1,0,0,0,0,0,0,1,1,0,0,0,1,0,1,1,0,0,0,0,1,0,1,0,0,1,0,1,1,1,1,1,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,0,1,1,0,0,0,0,0,1,0,0,1,1,0,1,1,0,0,1,0,1,1,1,1,1,1,1,1,0,1,1,1,1,0,1,0,1,1,1,1,0,0,0,0,1,1,1,1,1,0,1,0,1,1,0,0,0,1,1,0,0,1,1,0,0,0,0,0,1,1,0,1,0,1,0,1,0,1,0,1,1,1,1,1,0,1,1,1,0,0,1,0,1,1,1,0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,0,0,1,0,0,0,1,0,1,1,1,1,1,0,1,1,0,0,1,1,0,1,1,0,0,1,1,0,0,1,0,1,1,0,0,0,1,0,1,1,1,1,0,1,0,1,1,0,1,0,1,0,0,1,1,0,1,0,0,0,1,1,1,1,1,0,0,1,1,0,1,1,1,1,1,1,0,1,0,0,1,1,1,1,0,1,1,0,0,1,0,1,0,0,1,0,0,1,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,0,0,1,0]
number of clauses solved: 351 hex: 15f
number of atempts: 5 hex: 5
assignment of variables: [0,1,0,1,0,0,1,1,0,0,1,1,1,1,0,1,1,0,0,0,1,0,1,1,1,0,0,1,0,0,0,0,1,1,0,1,1,0,0,1,0,1,1,0,1,1,0,0,1,0,1,0,0,1,1,0,1,0,0,1,0,1,0,1,1,1,1,1,1,1,0,1,0,1,0,0,0,0,1,0,1,1,0,0,1,0,1,1,0,0,1,0,1,1,1,0,1,1,1,0,0,1,1,1,0,1,1,1,0,0,0,1,0,1,0,0,0,0,0,1,0,1,1,1,1,0,0,0,1,1,0,0,1,1,1,1,0,1,1,1,1,0,0,0,0,0,0,1,0,1,1,1,1,1,0,1,0,1,0,0,1,0,1,0,0,1,1,1,0,0,1,1,0,1,1,1,0,0,0,1,0,1,1,1,1,1,1,1,0,0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,1,0,1,1,0,0,1,0,1,1,1,0,1,1,1,1,0,1,0,1,0,0,1,1,0,1,0,0,1,1,0,0,0,1,1,0,1,0,1,1,0,1,0,0,1,1,0,0,0,0,1,1,0,1,0,1,0,1,0,0,1,0,0,0,1,0,0,1,1,1,0,0,1,0,0,1,0,0,0,1,1,0,1,0,0,1,1,1,0,0,1,0,0,0,0,0,1,1,0,1,1,1,1,0,1,0,1,1,1,1,0,1,0,1,0,1,0,1,0,1,1,0,1,0,1,0,0,1,0,0,0,0,1,0,0,1,0,0,1,1,0,0,0,1,1,1,0,1,0,0,0,1,0,1,0,0,0,1,1,0,1,1,0,1,1,0,0,1,1,0,1,0,0,0,0,1,0,1,1,0,0,0,1,0,0,0,1,1,1,0,0,1,1,1,0,1]
number of clauses solved: 357 hex: 165
number of atempts: 13 hex: d
assignment of variables: [0,1,0,0,0,0,0,0,1,0,1,1,1,1,1,0,1,0,0,0,1,1,0,1,0,0,1,1,0,0,1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,0,1,0,1,1,1,1,1,0,1,0,1,1,0,0,0,1,0,0,1,0,0,1,1,1,1,0,1,1,0,0,0,1,0,0,1,0,1,0,0,1,1,1,0,1,1,0,0,0,0,1,1,0,1,1,0,1,1,0,0,0,1,0,1,1,1,1,1,0,0,0,1,0,0,0,1,1,0,0,1,1,1,1,1,0,1,0,1,0,0,1,0,0,1,0,1,1,1,1,1,1,1,1,0,1,0,0,0,1,0,1,1,0,0,1,1,1,0,0,0,1,1,0,1,1,1,1,0,0,0,0,1,1,0,0,1,1,1,1,1,0,1,1,1,0,0,1,1,1,1,1,0,1,1,1,1,0,1,1,1,0,1,0,1,0,1,0,0,1,0,0,1,0,1,0,1,0,0,0,0,1,0,0,0,0,1,1,0,0,0,0,0,1,1,1,0,0,0,0,1,1,1,1,0,1,0,0,0,1,0,1,1,0,1,0,0,1,1,1,0,0,0,0,0,1,1,0,0,1,0,0,1,0,0,1,1,1,1,0,1,1,1,1,0,1,1,0,0,1,0,1,1,1,1,0,1,0,1,0,0,0,0,1,0,1,0,0,1,0,0,1,0,1,1,0,1,1,1,1,1,0,1,1,0,1,1,1,1,1,0,0,1,0,1,0,1,0,0,1,0,0,0,1,0,1,1,0,0,0,1,0,1,0,0,0,1,1,1,0,1,0,0,1,0,1,0,1,1,0,0,1,1,1,1,1,1,0,0,1,1,0,1,0,1,0,1,0,1,0]
number of clauses solved: 362 hex: 16a
number of atempts: 79 hex: 4f
assignment of variables: [1,0,1,1,0,1,0,1,0,1,1,1,0,1,1,0,1,1,1,0,1,0,1,1,1,1,0,0,0,1,1,0,0,0,1,1,1,0,1,1,1,0,0,0,0,1,0,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1,0,0,1,1,0,0,0,0,1,0,0,1,1,1,0,0,1,1,1,1,1,1,1,1,1,1,1,1,0,1,1,0,0,0,1,1,0,0,0,0,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,0,1,0,1,0,0,0,0,1,0,1,0,1,1,1,0,0,0,1,1,1,1,1,0,0,1,0,1,0,0,1,0,1,1,1,0,0,1,0,1,1,1,0,1,0,1,1,0,1,1,0,1,0,1,0,1,1,1,1,0,1,0,0,1,1,0,1,0,1,1,0,1,0,1,1,1,0,1,0,0,1,1,1,1,0,0,1,0,1,0,0,0,1,0,1,1,0,1,0,0,1,1,1,1,1,0,0,0,1,1,0,0,0,0,0,1,0,0,0,0,1,1,0,0,0,1,0,0,1,1,1,1,0,1,0,0,1,1,1,1,0,0,1,0,1,0,1,1,0,0,1,1,1,0,0,1,0,1,0,0,1,0,0,0,1,1,1,0,1,1,0,1,1,1,1,0,1,1,0,0,0,1,1,1,1,1,0,0,0,0,1,0,1,1,0,1,0,0,1,1,0,1,0,1,1,0,0,0,0,1,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,1,1,1,1,1,0,0,1,0,0,1,0,1,1,1,1,0,0,1,1,0,1,0,0,1,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,0,0,1,1,1,1,0,1,0,1,1]
number of clauses solved: 365 hex: 16d
number of atempts: 117 hex: 75
assignment of variables: [0,1,0,1,0,1,0,0,1,1,0,0,0,1,1,0,0,0,0,1,1,0,0,1,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,0,1,1,1,0,1,1,1,1,1,1,1,0,1,1,1,0,0,1,0,1,1,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,1,1,1,0,1,0,1,1,0,0,1,0,0,1,1,1,0,1,0,0,1,0,1,0,0,0,1,0,1,0,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,1,0,0,1,0,0,1,1,1,0,0,0,0,1,1,0,1,0,0,0,1,0,0,1,0,0,1,0,1,0,0,0,1,0,0,1,0,0,1,1,0,0,0,1,1,0,1,1,1,1,0,0,0,1,1,0,1,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0,0,1,1,1,1,0,0,1,1,0,1,1,1,1,0,1,0,1,1,1,0,1,0,1,1,1,1,1,0,0,1,0,1,1,0,1,0,1,0,1,0,0,1,0,1,0,0,0,1,0,0,0,0,1,0,1,1,1,1,1,0,1,1,1,0,1,0,0,1,0,1,1,0,1,0,1,0,0,0,0,1,0,1,1,0,0,0,1,1,1,1,0,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,0,1,1,1,1,0,0,0,0,1,0,1,0,0,0,0,0,0,1,0,0,1,1,1,1,0,0,1,1,1,0,0,1,0,1,0,0,1,0,0,0,0,0,1,0,0,1,0,0,0,0,0,1,0,0,0,1,1,1,1,1,0,0,1,1,0,1,0,1,0,1,0,0,1,0,1,0,0,1,1,0,1,0,0,1,0,1,0,1,0,1,1,0,1,1,0,1,0,1]
number of clauses solved: 366 hex: 16e
number of atempts: 133 hex: 85
assignment of variables: [0,0,1,0,0,0,0,0,0,0,1,1,0,0,1,1,1,0,0,0,1,1,0,0,0,0,0,1,0,1,0,1,0,1,1,0,0,0,0,1,0,1,0,0,1,1,0,1,0,1,1,0,0,0,1,0,1,1,1,0,0,1,1,1,1,0,1,1,1,1,0,0,0,0,0,1,0,1,1,1,0,0,1,1,0,1,0,1,1,1,1,1,0,1,1,0,1,0,0,0,0,1,0,1,0,1,0,1,1,1,1,0,1,0,0,0,1,1,1,1,1,1,0,0,0,0,0,1,0,1,1,1,1,0,1,1,0,0,1,0,0,0,0,1,0,0,0,0,0,1,0,0,1,0,1,0,1,1,0,0,1,0,0,0,1,1,0,0,0,1,1,1,1,1,0,1,0,0,0,1,1,1,1,1,0,1,1,1,1,1,0,1,0,1,0,0,0,1,1,1,0,0,1,1,1,0,1,0,0,0,1,1,1,1,0,1,0,0,1,0,0,0,1,1,1,1,1,1,0,1,1,1,0,0,0,0,1,1,0,1,0,0,0,1,1,0,0,0,1,0,0,0,0,0,0,1,1,1,1,1,1,1,0,1,0,0,1,0,1,1,0,1,0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,0,0,1,1,0,0,1,1,0,1,1,1,1,0,1,1,1,0,1,1,0,1,0,0,0,1,1,0,1,1,0,1,1,1,1,1,1,0,1,1,1,0,1,0,1,0,0,0,0,0,1,1,0,0,1,0,0,0,1,1,1,0,1,0,1,0,0,1,1,0,1,0,0,0,1,1,1,0,0,1,1,0,0,1,0,1,0,0,0,0,0,0,0,1,1,0,1,1,0,1,0,0,0,0,0,0,0,1,0,1,1,1,0]
number of clauses solved: 372 hex: 174
number of atempts: 1283 hex: 503
assignment of variables: [0,1,0,0,1,1,0,0,1,0,1,1,1,0,0,0,1,0,0,0,0,0,1,0,0,0,0,0,0,1,1,0,1,0,1,1,1,1,0,1,1,1,0,0,1,1,1,0,0,1,1,1,0,1,1,0,1,0,0,1,0,1,1,1,1,1,1,0,0,0,1,0,0,0,1,0,1,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,1,1,0,0,0,1,1,0,0,1,0,1,1,1,1,1,1,0,0,1,1,0,0,1,0,1,0,0,0,1,1,1,1,0,0,1,1,0,0,0,0,0,1,0,1,0,1,1,0,0,1,0,0,1,0,0,1,1,1,1,1,0,0,0,1,1,0,0,1,0,1,0,0,0,0,1,0,1,0,1,1,0,0,0,1,0,0,1,1,1,1,0,1,1,0,0,0,1,1,0,0,0,0,1,1,1,0,1,1,1,0,0,1,0,0,1,0,1,1,0,1,0,1,0,0,0,1,0,0,0,1,1,1,0,1,0,0,1,0,0,0,1,1,0,0,1,0,0,0,0,1,1,1,0,1,1,1,1,0,0,0,0,0,1,0,0,1,0,1,0,1,1,0,1,0,1,1,1,1,1,0,0,1,0,0,0,0,0,0,1,1,1,1,1,1,0,1,1,1,1,1,0,0,0,1,0,1,0,0,0,1,1,1,0,1,0,1,1,1,1,0,0,0,0,1,1,0,0,1,1,1,1,1,1,1,0,1,1,0,1,1,1,1,0,1,0,0,0,1,1,0,1,0,1,1,1,1,0,1,0,1,0,0,0,0,0,1,0,0,1,1,1,1,1,0,0,1,1,0,1,0,0,1,1,0,0,0,1,1,1,0,1,0,1,0,0,1,0,0,1,0,0,0,1,1,0,0,0]
number of clauses solved: 373 hex: 175
SATSolve: interrupted
real 0m29.049s
user 0m28.634s
sys 0m0.048s
loki@rurix 15:10:55 ~/CKUle/cse4401 $
loki@rurix 15:10:55 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 400 400
number of variables: 400 hex: 190
number of clauses: 400 hex: 190
max variable combinations:2582249878086908589655919172003011874329705792829223512830659356540647622016841194629645353280137831435903171972747493376 hex: 10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
number of atempts: 1 hex: 1
assignment of variables: [1,1,1,0,1,0,0,0,1,1,1,1,0,1,0,0,0,0,1,1,1,0,0,1,0,0,1,1,0,1,1,1,0,1,0,1,1,0,1,0,1,1,0,1,1,1,0,0,0,0,0,1,0,1,0,0,1,1,1,0,1,1,0,1,0,0,0,1,0,1,1,0,0,0,0,0,0,0,1,0,0,0,1,1,1,0,1,1,0,1,1,0,0,1,1,0,0,1,1,0,0,1,0,0,0,0,1,0,1,1,0,0,1,0,1,1,0,1,0,0,1,1,1,0,1,1,1,0,1,1,1,0,1,0,1,1,0,1,1,1,1,0,0,0,1,1,0,1,1,1,0,1,0,1,0,1,1,0,0,0,0,1,1,1,1,1,1,1,1,0,1,0,0,0,1,1,1,0,0,1,0,1,0,0,1,1,0,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,0,1,1,0,1,0,0,0,1,0,0,1,1,0,1,1,1,1,0,0,1,1,1,1,0,1,1,1,0,1,1,0,0,1,0,1,1,1,0,0,0,1,1,1,0,0,1,0,1,1,1,1,0,1,0,1,1,1,0,1,1,0,1,1,0,0,1,1,0,0,0,1,1,1,0,1,0,1,0,1,0,1,0,1,1,0,0,0,0,1,0,1,1,1,0,0,0,0,1,1,1,0,0,0,1,0,1,0,0,1,1,1,1,0,1,1,0,1,0,1,0,1,0,0,0,1,1,1,1,1,0,1,1,1,0,0,1,0,0,1,1,0,1,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,0,0,1,1,0,1,1,1,1,0,0,0,1,0,0,1,1,1,0,1,0,1,0,1,1,1,0,0,0,1,0,1,0,1,1,0,1,0,0,0]
number of clauses solved: 348 hex: 15c
number of atempts: 4 hex: 4
assignment of variables: [0,0,1,1,1,0,1,0,0,0,0,0,1,1,0,1,1,1,0,0,0,1,0,0,0,0,0,1,1,1,1,0,1,0,0,1,0,0,1,0,0,1,1,0,0,0,1,1,1,0,1,1,0,0,1,1,1,1,1,1,0,0,1,1,0,1,0,0,0,1,0,0,0,1,1,1,0,0,1,1,1,1,0,1,1,1,0,0,1,0,0,1,1,1,0,0,0,0,1,1,1,1,1,1,0,0,1,0,1,1,0,1,1,1,0,1,0,1,0,1,0,1,1,1,0,0,0,1,0,1,1,1,0,1,1,1,0,1,0,1,1,0,1,0,1,0,0,0,0,1,0,0,1,1,1,1,1,0,1,0,1,0,0,0,1,0,0,0,0,1,0,1,0,1,1,0,0,1,1,0,0,0,0,1,1,0,0,1,1,1,1,0,0,0,0,1,0,1,0,0,0,1,0,0,0,1,0,1,0,0,0,0,1,1,0,1,0,0,0,1,1,0,1,1,1,0,0,0,1,1,0,1,0,1,1,0,0,0,1,1,0,1,1,0,0,0,0,0,1,0,0,1,1,1,0,1,1,1,1,1,1,0,0,0,0,0,1,0,0,1,1,1,0,0,0,1,1,0,1,1,1,1,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,0,0,0,1,0,0,1,0,1,0,1,0,1,0,0,0,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,1,1,0,0,0,1,0,0,1,1,0,0,1,1,1,0,1,1,0,1,0,1,0,0,1,0,0,1,1,0,1,0,1,0,0,1,0,1,1,1,0,1,1,1,0,0,1,1,0,0,0,0,1,0,0,1,0,0,0,0,0,1,1,1,0,1,0,0,1,0,0,1]
number of clauses solved: 351 hex: 15f
number of atempts: 9 hex: 9
assignment of variables: [0,1,0,0,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,1,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,1,0,0,0,1,1,1,0,0,1,1,0,1,0,0,1,0,1,0,1,0,1,0,1,1,1,0,1,0,0,1,0,1,1,0,1,1,0,0,1,0,1,0,1,1,0,0,0,1,0,0,1,1,1,1,1,1,0,0,0,0,1,1,1,0,1,0,0,0,0,1,0,1,0,0,1,1,0,0,1,0,1,1,0,1,0,0,0,1,1,0,0,1,1,0,0,0,1,0,1,0,0,0,1,1,0,1,0,1,1,1,0,1,1,0,1,1,0,1,0,1,1,0,0,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,1,0,1,1,1,1,1,1,1,1,1,0,0,0,0,1,0,0,1,1,1,0,0,0,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,0,0,1,0,1,1,0,1,1,0,1,1,1,1,1,1,1,0,1,0,1,1,1,0,0,0,0,0,0,0,0,0,0,1,0,0,1,0,1,1,1,1,1,0,0,1,1,1,0,1,0,0,1,0,0,0,0,1,0,0,1,1,1,1,1,0,1,1,0,1,1,0,1,0,0,0,0,1,0,0,1,1,0,1,0,0,0,1,1,0,0,1,1,0,0,1,0,0,0,1,0,1,1,0,0,0,1,0,1,0,1,1,0,0,1,1,0,0,0,0,0,0,1,0,0,1,0,0,1,1,0,1,1,1,1,1,1,0,1,0,0,0,1,0,0,1,0,0,0,0,1,1,0,1,0,0,1,0,0,0,0,1,1,0,1,1,0,1,0,1,1,0,0,1,0,0,0,1]
number of clauses solved: 358 hex: 166
number of atempts: 15 hex: f
assignment of variables: [0,0,0,1,1,1,1,0,1,1,1,0,0,0,0,0,1,1,0,0,1,1,0,0,1,1,1,0,0,1,0,0,0,1,1,1,0,0,0,1,0,1,0,1,1,0,0,0,1,0,0,1,0,1,0,1,0,1,0,0,1,0,0,0,0,1,0,0,1,0,1,1,0,0,0,0,0,1,1,0,0,1,1,1,1,1,1,0,0,1,1,1,0,0,0,1,0,0,0,0,1,0,1,0,1,0,1,1,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,1,1,0,1,0,1,1,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,1,1,1,0,1,1,1,0,1,0,0,1,1,1,1,0,1,0,0,0,0,0,1,0,0,1,1,1,0,1,0,1,0,0,1,1,1,1,0,0,0,0,1,1,0,1,1,0,0,0,0,0,1,0,1,0,1,1,0,0,0,1,1,0,0,1,0,1,1,1,0,1,1,1,0,1,0,1,1,0,0,0,1,1,1,1,0,0,0,1,0,0,0,0,1,0,0,0,0,1,0,1,1,1,0,1,0,1,1,0,0,0,1,0,0,0,0,1,1,1,0,0,1,1,0,0,1,0,0,0,1,1,1,0,0,1,1,0,1,0,0,1,0,0,0,0,0,1,0,1,0,1,1,1,0,1,1,0,1,1,0,1,0,0,0,1,0,1,0,0,0,1,1,1,1,0,0,1,0,0,1,0,0,0,0,0,1,1,1,0,1,0,0,0,0,0,1,0,1,0,1,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,0,0,0,0,0,0,1,1,1,1,1,0,0,1,1,0,1,1,1,1,1,0,0,1,1,1,0,0,0,1,1,0,1,0,0,0,0,0,0]
number of clauses solved: 360 hex: 168
number of atempts: 24 hex: 18
assignment of variables: [1,1,1,1,0,0,0,0,0,0,1,1,1,0,1,0,0,1,1,1,1,0,1,0,0,1,0,1,0,1,1,0,0,0,0,0,0,0,0,1,1,1,1,1,0,1,0,0,0,0,0,0,0,0,1,0,1,0,1,0,0,1,0,1,1,1,1,1,0,1,1,1,1,0,1,1,0,1,0,1,1,1,0,1,1,1,0,0,1,1,1,0,1,0,1,1,0,1,1,0,0,1,0,1,0,1,1,0,0,0,1,0,1,0,0,1,1,1,1,0,0,1,0,1,0,1,1,1,0,1,0,0,0,0,0,1,0,0,0,1,0,0,0,1,1,1,0,1,0,0,1,1,1,1,0,1,1,1,1,1,0,1,1,0,1,1,0,0,0,0,0,0,1,0,1,1,0,0,0,0,1,1,1,1,1,1,1,0,0,1,1,1,1,1,0,0,1,1,1,1,1,0,1,0,0,1,1,1,0,1,0,1,1,1,0,0,1,0,1,1,1,1,1,0,1,0,1,1,0,0,1,1,1,0,1,1,1,0,0,0,0,1,1,0,1,0,1,1,1,0,1,0,0,0,1,1,0,0,0,1,1,1,0,0,1,1,1,0,0,0,1,0,0,1,1,0,0,0,1,0,1,0,0,1,1,0,1,1,0,0,1,0,1,1,1,0,0,0,0,1,1,1,1,1,0,1,0,0,0,1,0,1,1,0,0,0,1,1,1,0,1,1,0,1,0,1,0,0,1,1,0,0,1,0,0,0,0,1,1,0,1,0,1,0,0,0,1,0,0,0,0,1,1,0,1,1,0,0,0,0,0,1,1,0,1,0,0,1,0,1,0,0,1,0,0,1,1,0,1,1,1,1,1,0,1,1,1,0,0,0,0,1,1,1,1,1,0,0,0,0]
number of clauses solved: 363 hex: 16b
number of atempts: 29 hex: 1d
assignment of variables: [0,1,1,1,0,1,1,1,1,0,0,0,0,1,0,1,0,1,0,1,1,0,0,1,1,1,1,1,1,0,1,1,0,1,1,0,0,1,1,1,1,0,1,0,1,0,1,1,1,1,1,0,0,0,0,0,1,1,1,0,1,0,1,0,1,1,0,1,1,1,1,0,0,1,0,0,1,0,1,1,1,1,0,0,1,1,1,1,0,0,0,1,1,0,1,0,0,0,1,1,0,1,1,1,0,1,0,0,0,0,0,0,0,0,1,0,0,0,1,1,1,0,0,0,1,1,1,1,0,0,0,0,0,1,1,1,0,1,0,0,1,1,0,0,0,0,0,0,1,1,1,0,0,1,1,0,1,0,0,1,0,0,0,1,1,1,1,1,1,0,0,0,1,0,1,1,0,0,0,1,0,1,1,1,1,0,0,0,1,0,0,1,1,1,1,0,1,1,1,1,1,0,0,1,1,1,0,1,1,1,0,1,0,0,0,0,1,0,0,0,0,1,1,1,0,1,1,1,1,1,1,1,1,0,0,0,1,1,0,1,1,1,1,0,1,1,1,0,1,1,1,0,0,0,1,1,0,1,0,0,1,0,0,0,0,1,1,0,0,0,1,1,0,0,1,0,1,1,1,1,1,0,0,0,1,0,0,1,1,0,0,0,1,1,0,1,1,1,0,1,0,0,1,1,0,1,0,1,0,1,0,0,0,1,1,1,1,0,0,0,0,0,1,1,1,1,1,1,1,0,0,1,1,0,0,0,1,0,0,1,1,1,0,1,0,1,0,0,0,0,0,0,0,1,0,0,0,1,0,1,0,1,1,0,0,0,0,0,0,0,1,1,1,1,1,1,0,0,0,0,1,1,1,0,1,1,1,0,0,0,0,1,0,0,1,0,0,0,0,1]
number of clauses solved: 364 hex: 16c
number of atempts: 31 hex: 1f
assignment of variables: [0,1,1,1,1,1,0,1,0,1,0,0,1,1,0,1,1,1,1,0,0,0,1,0,0,0,0,0,0,1,1,0,0,1,0,0,0,1,0,0,0,0,0,0,1,1,1,0,1,1,1,1,1,0,1,1,0,0,1,0,0,1,0,0,0,0,1,1,0,1,1,1,0,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,1,0,1,1,0,0,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,1,1,1,1,1,1,1,1,0,1,1,1,1,1,1,0,1,0,1,1,1,1,0,0,0,1,1,0,1,1,0,1,0,0,0,1,1,0,1,0,1,0,0,0,1,1,0,0,1,1,0,0,1,0,0,1,1,1,1,1,0,0,1,1,0,0,0,1,0,1,0,0,1,1,0,0,0,1,0,1,1,0,0,1,1,0,0,1,0,1,0,0,1,0,0,0,1,0,1,0,0,1,1,0,1,1,0,0,0,1,1,1,0,1,1,1,0,1,0,0,0,0,1,0,1,0,1,0,0,1,1,0,1,1,0,0,0,1,1,1,0,0,1,1,0,0,0,0,0,1,1,0,0,0,1,1,0,1,1,0,1,1,0,1,0,1,1,0,0,1,0,0,0,1,0,1,1,1,1,1,1,0,1,1,0,1,0,0,0,1,1,0,0,0,1,1,1,0,0,0,1,0,1,0,1,0,1,1,1,1,1,1,1,0,0,1,1,0,0,0,0,0,0,1,1,1,1,1,1,1,0,1,1,1,1,1,0,1,1,0,1,0,0,0,0,1,0,1,1,0,0,0,1,1,1,0,1,0,0,1,0,0,1,0,0,1,1,0,0,1,0,1,1,1,1,0,1,1,1,0,0,0,0,1,1,0,0,1,0,1]
number of clauses solved: 367 hex: 16f
number of atempts: 228 hex: e4
assignment of variables: [1,0,1,1,1,0,1,1,1,0,0,1,0,0,1,0,0,0,0,0,1,0,1,1,1,0,1,0,1,1,1,0,1,1,1,1,0,0,0,0,0,1,1,0,0,1,1,0,0,0,1,0,0,1,0,0,0,0,0,1,1,0,1,1,0,1,0,1,0,0,1,0,1,1,1,1,0,1,1,0,0,1,0,1,0,1,0,0,1,0,0,1,1,1,1,0,0,0,0,1,0,1,1,1,1,1,1,1,0,1,0,0,1,0,1,1,1,1,1,1,1,1,0,0,1,0,0,0,0,0,0,1,0,1,0,1,1,1,1,0,1,0,0,1,0,1,0,1,1,0,0,0,1,0,1,0,1,0,1,0,1,0,0,0,1,0,0,0,0,1,0,0,1,0,1,1,1,1,1,0,0,1,1,0,0,1,0,0,0,1,1,1,0,1,0,0,0,0,0,1,1,1,1,0,0,1,0,0,1,0,0,1,1,0,1,1,0,1,0,1,1,0,0,1,0,0,1,1,1,0,1,0,0,1,1,0,1,1,1,1,1,1,0,1,1,1,1,1,1,1,0,1,0,1,0,1,0,1,1,1,0,1,0,0,0,1,1,0,1,1,0,0,0,1,0,1,1,1,1,1,0,1,0,0,1,0,1,0,1,0,0,0,1,0,1,0,1,0,1,0,1,1,0,0,1,0,1,0,0,1,0,1,1,1,0,1,0,0,0,1,1,1,0,1,1,1,1,1,0,1,0,0,1,1,0,1,0,1,1,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,1,0,1,0,1,1,0,1,0,0,1,0,1,1,0,1,1,0,0,1,0,1,1,0,1,0,1,0,0,0,1,0,1,0,0,1,1,1,0,0,0,1,1,1,0,0]
number of clauses solved: 370 hex: 172
number of atempts: 2622 hex: a3e
assignment of variables: [0,1,1,1,0,0,0,1,1,0,0,1,0,0,1,1,1,1,0,1,0,1,0,0,1,1,1,1,1,0,0,0,0,0,0,1,0,0,0,1,1,1,0,1,1,1,1,1,1,1,1,1,0,1,0,1,1,0,1,1,0,1,0,1,1,0,0,1,0,1,1,1,1,1,1,1,1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,0,0,1,1,1,0,0,0,0,1,0,1,0,1,1,1,1,0,0,1,0,0,1,0,0,1,0,1,1,1,1,1,0,0,0,1,0,1,0,0,1,1,0,0,1,1,1,0,0,1,0,0,1,0,1,0,1,0,1,0,0,1,1,1,1,0,1,1,1,1,1,0,0,0,0,0,0,0,1,1,1,1,0,1,1,1,1,1,1,0,0,1,0,1,1,0,1,1,0,0,1,1,0,1,1,0,0,1,0,0,0,1,0,0,0,1,0,0,1,1,0,0,0,0,1,1,1,0,0,1,1,1,1,1,0,1,1,0,1,1,1,0,1,0,1,0,1,0,0,0,1,0,0,1,0,1,0,0,1,0,0,1,0,0,0,0,1,1,1,1,1,0,1,1,1,1,0,0,0,0,0,0,0,0,1,1,0,1,1,0,0,1,1,0,1,1,0,0,0,0,0,1,1,1,0,0,1,0,1,0,0,1,0,0,1,0,1,0,1,0,0,1,1,1,0,1,0,1,0,0,1,1,0,0,1,0,1,0,0,1,1,0,0,1,0,1,0,1,1,1,0,0,1,0,1,0,1,1,1,0,0,1,1,1,1,1,1,0,1,0,0,1,1,0,1,0,1,0,1,1,1,0,0,0,0,0,0,0,0,1,1,1,1,0,1,0,0,0,0,1,1,1,0,0,1,0,1,0,1]
number of clauses solved: 372 hex: 174
number of atempts: 6149 hex: 1805
assignment of variables: [1,0,1,1,1,1,0,1,0,1,1,1,1,0,0,1,0,1,0,1,1,1,0,1,0,1,0,0,0,0,0,1,0,1,0,1,0,0,1,0,0,1,0,1,1,0,1,1,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,1,1,0,0,1,0,0,1,1,0,1,1,1,0,1,0,0,0,0,1,0,1,1,1,0,1,1,1,1,0,0,1,1,1,1,0,0,0,0,0,1,0,1,1,1,1,0,1,1,1,0,1,0,0,1,0,0,0,1,1,0,1,0,1,0,1,0,0,1,1,0,0,0,1,0,0,0,0,1,0,1,0,0,0,1,1,1,0,1,0,0,1,0,0,1,0,1,1,0,1,0,0,0,1,0,1,1,1,0,1,0,1,1,0,1,0,0,0,1,1,0,1,1,0,0,0,1,0,1,1,0,0,1,1,1,1,1,1,0,0,0,0,0,1,0,1,1,0,1,1,1,1,1,1,0,1,0,1,0,0,0,0,0,1,1,0,1,1,0,0,0,0,1,1,0,1,1,1,0,1,0,1,0,1,1,1,1,1,1,1,1,1,1,1,0,0,1,0,0,1,0,1,1,0,1,0,0,1,0,1,1,1,0,1,1,1,1,0,0,0,1,1,1,0,0,0,1,0,1,1,0,1,1,1,1,0,1,0,0,0,1,0,1,0,0,0,0,0,0,1,1,1,0,0,1,0,0,0,1,0,1,1,1,1,1,0,1,0,1,0,0,0,0,1,0,1,0,0,1,1,0,1,0,0,1,1,1,0,0,0,0,1,0,0,1,1,0,0,1,1,1,0,1,0,0,0,1,1,1,1,1,0,1,0,0,0,1,1,1,1,1,0,0,1,1,1,0,0,1,1,0,0,1,0,1,1,0]
number of clauses solved: 375 hex: 177
SATSolve: interrupted
real 6m44.456s
user 6m40.529s
sys 0m0.664s
loki@rurix 15:19:58 ~/CKUle/cse4401 $
Version 1.1.1
loki@rurix 15:41:51 ~/CKUle/cse4401 $ cp /home/loki/skamSELypla/sat/dist/build/SATSolve/SATSolve ~/bin
loki@rurix 15:42:16 ~/CKUle/cse4401 $ CNFGenerate 32 64 3 > prob1.cnf
loki@rurix 15:42:21 ~/CKUle/cse4401 $ CNFGenerate 64 128 3 > prob2.cnf
loki@rurix 15:42:26 ~/CKUle/cse4401 $ CNFGenerate 128 256 3 > prob3.cnf
loki@rurix 15:42:33 ~/CKUle/cse4401 $ time SATSolve prob1.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 32 64
number of variables: 32 hex: 20
number of clauses: 64 hex: 40
max variable combinations:4294967296 hex: 100000000
assignment of variables: [0,1,0,1,0,0,1,1,1,1,0,1,1,1,1,0,1,0,1,0,0,0,1,1,0,0,1,0,1,0,1,0]
number of clauses solved: 56 hex: 38
number of atempts: 1 hex: 1
assignment of variables: [1,0,0,0,1,0,1,1,1,1,1,1,1,0,1,1,1,1,1,0,1,0,1,1,1,1,1,1,0,1,1,0]
number of clauses solved: 59 hex: 3b
number of atempts: 3 hex: 3
assignment of variables: [1,1,1,1,1,0,1,1,1,0,1,1,0,1,0,0,0,1,0,1,1,0,1,1,0,1,1,1,0,0,1,0]
number of clauses solved: 61 hex: 3d
number of atempts: 8 hex: 8
assignment of variables: [1,1,0,1,0,0,1,1,0,1,0,1,0,0,0,0,1,0,1,0,1,0,1,1,0,1,0,1,1,0,0,0]
number of clauses solved: 62 hex: 3e
number of atempts: 12 hex: c
assignment of variables: [1,0,0,1,1,1,0,1,1,0,0,1,0,1,0,0,0,1,0,1,1,0,1,1,1,0,1,1,0,1,1,0]
number of clauses solved: 63 hex: 3f
number of atempts: 178 hex: b2
assignment of variables: [1,0,0,0,0,0,1,1,1,1,0,1,0,0,0,0,1,0,0,1,0,1,1,1,0,1,1,1,0,1,1,1]
number of clauses solved: 64 hex: 40
number of atempts: 299 hex: 12b
SATisfiable
real 0m0.061s
user 0m0.052s
sys 0m0.004s
loki@rurix 15:42:47 ~/CKUle/cse4401 $ time SATSolve prob2.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 64 128
number of variables: 64 hex: 40
number of clauses: 128 hex: 80
max variable combinations:18446744073709551616 hex: 10000000000000000
assignment of variables: [1,1,0,1,0,0,0,1,1,0,0,0,0,0,0,0,0,0,1,0,1,0,0,1,1,0,0,1,1,1,1,1,0,1,0,1,1,1,1,0,1,0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,0,1,1,0]
number of clauses solved: 118 hex: 76
number of atempts: 1 hex: 1
assignment of variables: [1,1,1,1,1,1,1,1,0,1,1,0,1,1,0,0,0,1,1,1,1,1,1,0,0,0,1,1,1,1,1,0,1,1,0,1,1,1,0,1,1,0,0,1,0,1,1,1,1,1,0,0,1,1,0,0,0,0,0,1,0,0,1,0]
number of clauses solved: 122 hex: 7a
number of atempts: 17 hex: 11
assignment of variables: [0,1,0,0,0,1,0,0,0,0,1,0,0,0,0,0,0,0,1,1,1,0,0,0,1,0,1,0,0,0,0,0,0,1,1,1,0,1,0,1,1,1,0,0,1,1,1,1,1,1,1,1,0,0,0,0,1,0,1,0,0,0,1,1]
number of clauses solved: 123 hex: 7b
number of atempts: 514 hex: 202
assignment of variables: [0,1,1,1,1,0,1,0,0,1,1,0,1,1,1,0,1,0,1,0,0,1,0,1,0,0,1,0,0,1,0,1,1,1,0,1,1,1,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0,1,1,0,0,0,1,0,1,0,0]
number of clauses solved: 125 hex: 7d
number of atempts: 2606 hex: a2e
assignment of variables: [0,1,1,0,0,0,1,0,0,0,1,1,0,1,1,1,0,0,0,1,1,1,1,1,1,0,0,1,0,1,1,0,1,1,1,0,0,0,0,0,1,0,0,1,0,0,1,1,0,1,1,1,0,1,1,1,0,0,1,0,0,1,0,0]
number of clauses solved: 126 hex: 7e
number of atempts: 274881 hex: 431c1
bah it finished but my TMOUT variable wasn't unset so the bash session ended
loki@rurix 17:53:40 ~/CKUle/cse4401 $ stay
loki@rurix 17:54:03 ~/CKUle/cse4401 $ SATSolve prob2.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 64 128
number of variables: 64 hex: 40
number of clauses: 128 hex: 80
max variable combinations:18446744073709551616 hex: 10000000000000000
assignment of variables: [1,0,0,1,1,0,0,0,1,0,0,0,1,1,1,1,0,0,1,1,1,0,1,1,1,1,0,1,1,1,1,1,0,0,1,0,0,0,1,1,1,0,1,1,1,0,0,0,1,0,0,0,1,0,0,1,0,1,0,1,0,1,1,0]
number of clauses solved: 112 hex: 70
number of atempts: 1 hex: 1
assignment of variables: [1,1,0,0,1,1,0,1,0,0,0,1,0,1,0,1,1,0,1,0,0,0,0,1,1,0,1,0,0,0,1,0,0,1,0,0,0,0,1,0,1,0,0,0,0,1,1,1,1,0,1,0,1,0,1,1,0,0,1,0,0,1,1,0]
number of clauses solved: 114 hex: 72
number of atempts: 11 hex: b
assignment of variables: [0,0,0,1,1,0,1,0,0,0,0,1,1,0,1,0,0,1,0,1,1,0,1,0,1,0,0,0,1,1,0,1,0,0,1,0,0,1,0,0,0,0,0,1,0,0,1,1,0,1,1,0,1,0,1,1,1,0,1,0,1,0,0,0]
number of clauses solved: 116 hex: 74
number of atempts: 12 hex: c
assignment of variables: [1,1,1,0,0,0,0,0,1,1,0,0,1,0,1,0,1,1,1,0,1,1,0,0,1,0,0,0,1,1,0,0,0,1,0,1,0,0,0,0,0,1,0,0,1,1,1,1,0,1,0,0,0,1,0,1,0,0,1,1,0,1,1,1]
number of clauses solved: 122 hex: 7a
number of atempts: 15 hex: f
assignment of variables: [1,1,1,0,1,0,0,1,0,0,1,0,1,0,0,1,0,1,0,1,0,1,1,0,0,0,0,1,0,1,0,0,1,0,0,1,0,1,0,0,0,0,0,1,0,1,0,1,1,0,1,0,0,1,0,1,1,0,1,0,1,0,1,1]
number of clauses solved: 124 hex: 7c
number of atempts: 3610 hex: e1a
assignment of variables: [1,1,0,0,1,1,1,0,1,1,0,0,1,1,1,1,0,1,1,0,0,1,0,1,1,0,0,1,0,1,1,1,1,1,1,1,0,1,0,0,1,1,0,0,0,1,1,0,0,1,0,0,1,0,1,1,0,0,1,0,0,1,0,1]
number of clauses solved: 125 hex: 7d
number of atempts: 50035 hex: c373
This would be a good benchmarking tool to check for CPU speed and the randomness of random number generators.
assignment of variables: [0,1,0,0,1,0,1,1,0,0,0,0,1,1,0,1,1,0,1,0,0,1,0,0,1,0,0,0,0,0,0,1,1,1,0,1,0,1,0,0,0,1,0,1,1,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,0,0,1,0]
number of clauses solved: 126 hex: 7e
number of atempts: 542485 hex: 84715
I mis-speled atempts on purpose as an anti-double-consonants kind of thing
It's just a matter of time before a solution is found.
The better (least repeating sequences) in the random number generator the faster the result would be found.
can find more info at http://tcana.info
assignment of variables: [0,1,1,0,1,1,0,1,1,0,0,0,1,0,1,1,1,1,0,0,0,1,0,0,1,0,1,1,1,1,1,0,1,1,0,1,0,0,1,0,1,1,0,0,1,1,1,1,1,1,0,0,0,0,1,0,0,0,0,1,0,0,1,0]
number of clauses solved: 127 hex: 7f
number of atempts: 2734177 hex: 29b861
assignment of variables: [0,1,1,1,1,0,1,0,0,1,0,1,1,1,0,1,1,1,1,0,0,1,0,0,0,0,0,0,0,1,0,0,1,0,0,1,0,1,0,0,1,1,0,0,1,1,1,0,1,1,1,0,1,1,1,0,0,1,1,0,0,0,0,0]
number of clauses solved: 128 hex: 80
number of atempts: 3051300 hex: 2e8f24
SATisfiable
loki@rurix 18:11:06 ~/CKUle/cse4401 $
Bah forgot to time it. oh well you get the general idea roughly 17 minutes with my CPU and standard Haskell Random Number Generator
loki@rurix 21:28:02 ~ $ cat /proc/cpuinfo
processor : 0
vendor_id : AuthenticAMD
cpu family : 6
model : 8
model name : AMD Athlon(tm) XP 2400+
stepping : 1
cpu MHz : 2000.676
cache size : 256 KB
fdiv_bug : no
hlt_bug : no
f00f_bug : no
coma_bug : no
fpu : yes
fpu_exception : yes
cpuid level : 1
wp : yes
flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse syscall mmxext 3dnowext 3dnow ts
bogomips : 4004.80
clflush size : 32
loki@rurix 21:28:07 ~ $
loki@rurix 06:00:35 ~/CKUle/cse4401 $ time SATSolve prob3.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 128 256
number of variables: 128 hex: 80
number of clauses: 256 hex: 100
max variable combinations:340282366920938463463374607431768211456 hex: 100000000000000000000000000000000
assignment of variables: [1,0,0,1,0,1,0,0,0,1,1,1,0,0,0,1,0,1,1,1,1,1,1,1,0,1,1,1,0,0,0,0,1,1,1,1,1,1,0,0,1,0,0,1,1,1,1,1,0,1,0,1,1,0,1,0,0,1,0,1,1,0,1,1,0,0,0,0,0,1,1,0,1,1,1,0,1,0,1,1,0,1,1,0,0,0,0,1,0,1,0,1,0,0,0,1,1,1,1,1,1,1,1,1,0,0,0,1,0,1,0,0,1,1,0,0,1,1,1,0,0,1,1,0,1,1,0,0]
number of clauses solved: 217 hex: d9
number of atempts: 1 hex: 1
assignment of variables: [1,0,1,1,0,0,0,0,1,0,0,0,0,0,0,1,1,0,1,0,0,0,1,1,0,1,1,0,0,1,1,1,1,0,1,1,1,1,0,1,1,0,0,1,0,1,1,0,0,0,0,1,0,1,0,1,0,1,0,1,0,0,0,0,0,1,1,1,1,1,1,0,0,1,0,0,1,0,0,1,1,0,1,0,1,0,1,0,0,0,1,1,1,0,1,1,0,1,1,0,1,0,1,1,1,0,0,0,1,1,0,0,0,1,1,0,0,0,0,0,1,1,0,0,1,1,1,1]
number of clauses solved: 225 hex: e1
number of atempts: 2 hex: 2
assignment of variables: [1,0,0,1,0,1,0,0,1,1,1,1,1,1,1,0,0,1,1,1,0,0,0,0,0,1,1,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,1,1,1,1,1,0,1,0,1,1,1,0,0,0,0,0,0,1,0,1,0,0,1,0,0,0,0,0,1,1,1,1,0,0,0,0,0,1,0,0,1,0,0,1,1,0,1,0,1,0,1,0,1,1,1,1,1,0,1,0,1,1,0,1,1,1,1,1,0,1,1,1,0,1,0,0,1,1,1,0,1,1,0,1,1,0]
number of clauses solved: 230 hex: e6
number of atempts: 5 hex: 5
assignment of variables: [0,1,1,0,0,0,1,1,0,0,0,0,0,0,1,1,0,0,1,0,1,1,0,0,0,0,1,1,1,0,1,1,0,0,1,1,0,0,0,1,1,0,1,1,1,0,0,1,0,1,1,1,0,0,1,0,0,0,1,1,1,1,0,0,0,1,0,1,0,1,0,0,1,0,1,1,1,0,0,0,0,0,1,1,0,0,1,1,0,1,1,0,1,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,1,1,1,0,1,1,0,1,1,0,1,0,1,0,1,1,1,1,1,1]
number of clauses solved: 238 hex: ee
number of atempts: 8 hex: 8
assignment of variables: [0,0,0,1,0,1,1,0,0,0,1,0,1,0,1,1,0,1,0,1,0,0,1,1,0,0,1,1,0,0,1,0,0,1,1,0,0,1,1,1,0,1,0,0,1,1,0,1,1,1,0,1,1,1,1,0,1,1,0,0,1,1,1,1,0,0,1,0,1,1,0,1,1,0,0,1,1,1,1,1,0,1,0,0,0,0,0,1,0,1,1,1,0,1,1,0,0,1,0,0,0,1,1,0,1,0,0,1,0,0,0,0,0,1,1,0,1,0,1,1,1,1,0,1,0,0,1,1]
number of clauses solved: 239 hex: ef
number of atempts: 269 hex: 10d
assignment of variables: [1,0,0,1,0,0,0,0,1,1,0,1,0,1,0,0,1,1,1,0,1,0,0,0,1,0,0,0,0,0,1,0,0,0,1,1,0,1,0,0,1,0,1,1,1,1,1,1,0,0,0,1,1,0,1,1,1,1,0,0,1,0,1,0,0,0,1,0,1,0,1,0,0,0,1,1,1,0,0,0,0,1,1,1,0,0,0,1,1,0,0,0,0,1,0,0,1,0,0,0,0,0,0,0,1,1,0,0,0,1,1,0,1,0,1,1,0,0,0,0,0,0,1,0,1,0,1,1]
number of clauses solved: 241 hex: f1
number of atempts: 1263 hex: 4ef
assignment of variables: [1,1,1,0,1,1,0,1,1,0,0,0,1,0,0,0,1,0,0,0,1,0,0,1,1,0,1,0,0,1,1,1,0,1,1,1,1,0,1,0,0,0,1,1,1,1,1,1,1,1,0,0,1,1,0,0,0,1,1,1,1,1,1,0,1,0,0,1,0,1,1,0,1,1,1,1,1,1,0,1,0,1,0,0,0,1,1,0,1,0,0,0,0,1,1,1,1,1,1,0,1,0,0,1,0,0,1,0,1,0,0,0,1,0,1,1,1,0,1,0,0,1,0,1,1,0,0,0]
number of clauses solved: 242 hex: f2
number of atempts: 6966 hex: 1b36
assignment of variables: [1,1,0,1,1,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0,1,1,1,1,0,0,1,1,1,0,1,0,0,1,1,1,1,1,0,0,0,0,1,0,0,1,1,1,1,0,1,1,0,1,1,0,1,1,0,1,1,1,1,1,1,1,0,0,1,0,1,1,0,0,1,0,1,0,1,1,0,0,1,1,0,1,1,1,1,0,0,1,0,1,0,1,1,1,0,1,1,0,1,1,0,0,1,1,0,0,0,0,1,1,0,1,0,0,1,1,1,0,1,1,1]
number of clauses solved: 243 hex: f3
number of atempts: 15882 hex: 3e0a
assignment of variables: [0,1,1,1,1,1,0,0,1,0,0,0,1,1,1,1,1,1,1,0,1,0,0,0,1,0,1,0,0,1,0,0,1,0,0,1,0,1,1,1,0,1,1,1,1,1,1,0,0,1,0,1,1,0,0,1,0,1,1,0,0,1,0,1,0,0,1,0,1,0,1,1,1,1,0,0,1,1,0,0,0,1,1,1,1,1,1,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,0,0,1,1,1,0,1,0,1,0,1,1,1,1,0,0,1,1,0,1,1,1,1,0,1,1]
number of clauses solved: 244 hex: f4
number of atempts: 255946 hex: 3e7ca
assignment of variables: [1,0,0,1,0,1,0,0,1,0,0,0,1,0,0,1,0,0,1,1,1,0,0,0,1,0,1,0,0,1,0,0,0,1,1,1,0,1,0,1,0,0,0,1,0,1,1,1,1,0,0,0,1,0,0,1,0,1,1,1,1,0,0,1,1,1,1,0,1,0,1,1,0,1,0,0,1,1,1,0,0,0,0,0,0,1,1,0,1,1,1,0,0,1,1,1,1,1,0,0,1,0,0,1,0,0,1,0,0,1,1,1,1,0,1,0,0,0,0,0,0,0,0,0,1,0,0,0]
number of clauses solved: 245 hex: f5
number of atempts: 1027797 hex: faed5
assignment of variables: [0,0,1,1,0,0,1,0,1,0,0,1,0,0,1,0,0,0,0,0,1,0,0,0,1,1,1,0,1,0,1,0,1,1,1,0,1,0,1,1,0,1,0,1,1,0,0,1,1,1,1,0,0,1,1,1,1,1,0,0,1,0,1,1,1,0,1,0,1,1,0,0,0,1,0,1,1,0,0,0,0,0,1,1,0,1,0,0,1,0,1,0,0,1,0,1,1,0,1,0,0,1,1,0,1,1,1,0,0,1,0,0,1,1,0,1,1,0,0,1,0,1,1,0,1,1,0,0]
number of clauses solved: 246 hex: f6
number of atempts: 1149867 hex: 118bab
assignment of variables: [0,1,1,1,1,1,0,0,0,0,0,1,0,1,0,1,1,1,0,1,0,0,1,0,1,1,1,1,0,0,1,1,1,1,0,0,1,0,0,0,1,0,0,1,1,0,0,1,0,1,0,0,0,1,1,0,1,1,0,0,1,1,1,1,1,0,1,0,1,0,1,0,1,0,0,0,0,0,1,0,0,1,0,1,1,0,1,1,0,0,1,0,1,0,1,0,1,0,1,1,0,1,1,1,1,1,1,0,0,0,0,0,1,1,0,1,1,1,1,1,1,0,1,1,1,1,1,1]
number of clauses solved: 247 hex: f7
number of atempts: 1601999 hex: 1871cf
assignment of variables: [0,1,1,1,0,0,1,0,0,1,0,0,1,0,0,1,0,0,0,1,1,1,0,0,0,1,0,0,0,0,0,1,0,1,1,0,1,0,1,0,0,0,1,1,1,1,0,1,1,1,1,1,0,1,1,0,1,1,0,1,0,0,1,0,1,1,1,1,1,0,1,1,1,0,0,0,1,1,1,0,0,0,1,0,1,0,0,0,0,1,1,0,1,1,1,1,1,0,0,1,1,1,1,1,0,1,0,0,0,0,0,0,1,1,1,0,1,0,1,1,0,0,1,0,0,1,1,0]
number of clauses solved: 248 hex: f8
number of atempts: 7603098 hex: 74039a
assignment of variables: [1,1,1,0,1,0,1,0,1,1,1,1,1,1,0,1,0,1,1,0,0,0,1,0,1,1,1,0,0,0,0,1,0,1,1,0,1,0,1,0,1,0,0,1,1,1,0,1,1,1,0,0,1,1,1,1,1,1,1,0,1,1,0,0,0,0,1,0,1,0,1,0,0,0,1,1,1,0,0,0,0,0,1,1,0,1,1,1,0,1,0,0,0,0,0,1,1,0,0,0,1,0,0,0,1,1,0,1,0,0,1,0,0,0,1,0,1,0,1,1,1,1,0,0,0,1,1,1]
number of clauses solved: 249 hex: f9
number of atempts: 30690241 hex: 1d44bc1
in a perfect SAT-Solver none of those atempts would have used the same variable asignment -- depends on the random number generator realy, though it could be programmed in to store all the combinations the RAM usage and CPU time of checking would be prohibitive considering the number of atempts.
assignment of variables: [1,0,0,1,0,0,0,0,1,0,0,0,0,1,0,0,0,1,0,1,0,0,0,0,1,0,1,1,1,0,0,0,0,0,1,0,0,1,1,1,1,0,0,0,1,0,0,1,1,1,1,0,0,1,1,1,0,1,0,1,1,0,0,1,1,1,1,1,0,0,0,1,0,1,0,0,1,1,0,0,0,0,0,0,0,1,1,1,0,0,1,0,1,1,1,1,1,0,0,1,0,0,0,0,1,0,1,0,1,0,0,1,0,1,1,0,1,0,0,1,1,0,1,1,0,1,1,1]
number of clauses solved: 250 hex: fa
number of atempts: 78822483 hex: 4b2bc53
so the likelyhood of getting 250 clauses solved on first random assignment with this random number generator is roughly 1:4b30000 or 1 in 79 million
if it was perfectly random could solve all clauses on the first try.
real 2944m46.093s
user 2893m23.754s
sys 5m44.958s
loki@rurix 07:05:26 ~/CKUle/cse4401 $
WqdeVk
loki@rurix 07:05:26 ~/CKUle/cse4401 $ CNFGenerate 128 128 3 > prob3.cnf
loki@rurix 07:06:19 ~/CKUle/cse4401 $ time SATSolve prob3.cnf
loki@rurix 07:05:26 ~/CKUle/cse4401 $ CNFGenerate 128 128 3 > prob3.cnf
loki@rurix 07:06:19 ~/CKUle/cse4401 $ time SATSolve prob3.cnf
Loki's Shunso CNF Categorizer
header of CNF file:
c Generated by Loki's Random CNF Generator coded in Haskell
p cnf 128 128
number of variables: 128 hex: 80
number of clauses: 128 hex: 80
max variable combinations:340282366920938463463374607431768211456 hex: 100000000000000000000000000000000
assignment of variables: [1,0,1,1,1,1,0,1,1,0,1,0,1,1,0,1,1,0,1,1,1,1,1,0,1,0,1,0,1,0,0,0,1,0,1,1,0,1,1,1,0,1,1,0,0,1,1,0,1,0,0,0,0,0,0,1,0,0,1,1,0,1,1,0,0,0,0,0,0,1,0,0,0,1,1,1,1,0,1,1,0,0,1,0,1,0,0,0,0,1,0,0,1,1,0,0,1,1,0,1,1,1,0,1,0,1,1,1,1,0,0,1,1,1,1,1,0,0,1,1,0,1,0,1,1,1,1,0]
number of clauses solved: 108 hex: 6c
number of atempts: 1 hex: 1
assignment of variables: [1,1,1,1,0,1,1,0,1,1,1,1,1,0,0,1,0,1,1,0,1,0,0,0,0,1,0,0,0,0,1,1,1,1,1,1,0,1,1,1,1,1,1,0,0,0,0,1,1,1,1,0,0,0,0,1,0,1,0,1,0,1,0,1,1,1,1,1,0,0,1,0,0,0,1,1,0,0,1,0,1,1,1,1,0,1,0,0,0,0,1,1,1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,0,1,0,0,0,1,1,0,1,1,1,0,0,0,1,1,0,0,1,0,1]
number of clauses solved: 113 hex: 71
number of atempts: 2 hex: 2
assignment of variables: [0,0,0,0,1,1,1,1,1,0,0,1,1,0,1,0,0,1,0,0,1,0,1,0,0,1,0,1,1,1,0,1,0,1,0,0,0,1,1,1,1,1,0,1,1,1,0,1,1,0,1,1,0,1,0,0,1,1,0,1,1,1,0,0,0,0,0,0,1,0,0,0,0,1,0,0,1,1,1,0,1,1,0,1,1,0,0,0,1,1,1,1,0,1,0,1,0,0,1,0,0,1,1,1,1,0,1,0,0,1,1,0,0,1,0,0,0,0,0,0,1,0,0,0,0,1,1,0]
number of clauses solved: 117 hex: 75
number of atempts: 3 hex: 3
assignment of variables: [1,0,0,1,0,1,1,0,0,1,0,0,1,1,1,1,0,0,1,1,1,1,1,0,1,1,1,0,1,0,0,0,0,1,1,1,1,1,0,0,1,0,0,0,1,1,0,1,1,1,1,1,0,0,0,1,0,0,0,1,1,0,1,1,0,0,1,0,0,0,0,1,0,0,1,0,0,1,1,0,0,0,1,1,0,0,1,0,1,0,1,1,1,1,0,0,0,0,1,1,0,1,1,1,0,1,0,0,0,1,0,0,1,1,0,1,1,1,0,1,1,0,1,0,1,0,0,0]
number of clauses solved: 122 hex: 7a
number of atempts: 20 hex: 14
assignment of variables: [1,0,1,1,1,0,1,0,0,1,1,1,1,0,1,1,1,1,0,0,1,0,1,1,1,1,0,0,1,0,0,1,0,1,0,0,0,0,1,1,0,1,1,0,1,1,0,0,0,1,1,1,1,1,0,0,0,1,0,1,0,1,1,0,1,1,0,1,0,1,0,1,0,1,0,1,1,1,1,1,0,0,0,1,0,0,0,1,1,0,0,1,1,1,0,0,0,0,0,1,0,0,0,0,1,0,1,0,1,1,1,0,0,1,0,0,0,0,1,0,1,1,0,1,1,0,1,0]
number of clauses solved: 123 hex: 7b
number of atempts: 111 hex: 6f
assignment of variables: [1,1,1,0,1,1,1,1,1,0,0,1,1,1,0,0,0,0,1,0,0,1,0,1,1,0,1,0,0,0,0,0,1,1,0,0,0,1,1,1,0,0,0,1,1,1,0,1,0,1,0,1,1,0,0,0,0,0,1,1,0,0,0,0,0,1,0,1,0,0,1,1,0,0,0,0,0,0,0,1,1,1,1,0,0,1,0,1,0,0,1,0,0,0,0,1,1,0,0,1,1,0,0,0,0,1,1,0,0,1,0,1,1,0,0,0,0,0,0,1,0,1,1,1,0,0,0,0]
number of clauses solved: 124 hex: 7c
number of atempts: 2773 hex: ad5
assignment of variables: [1,0,1,1,1,1,1,0,0,1,0,1,1,0,0,0,1,0,1,0,0,0,0,0,1,1,0,0,0,1,1,0,0,0,0,1,0,1,0,1,1,1,0,1,1,1,0,0,1,0,1,1,1,0,1,0,1,1,1,0,0,1,1,1,1,1,0,1,1,0,1,1,1,1,0,0,0,0,1,1,0,1,0,1,1,0,0,0,1,1,1,1,0,0,0,1,1,0,1,1,0,0,1,1,0,0,1,1,1,1,0,0,1,0,1,0,0,0,0,1,1,1,0,0,1,0,0,0]
number of clauses solved: 125 hex: 7d
number of atempts: 23124 hex: 5a54
assignment of variables: [1,1,1,1,1,1,1,1,0,1,0,1,1,1,0,1,0,1,0,1,1,1,1,1,0,1,0,1,0,0,0,1,0,1,0,1,1,1,0,0,0,1,1,1,0,0,1,0,0,1,0,0,1,0,1,1,1,0,1,1,0,1,1,0,1,0,1,0,0,1,1,0,0,0,1,0,0,0,1,0,0,1,0,1,1,0,1,1,1,0,1,1,0,1,1,1,1,1,0,1,1,0,0,1,0,1,0,1,0,1,0,0,0,1,0,0,1,0,1,0,0,0,1,1,1,1,0,0]
number of clauses solved: 126 hex: 7e
number of atempts: 119069 hex: 1d11d
assignment of variables: [1,1,0,1,0,1,1,0,0,1,1,1,1,0,1,1,1,1,1,1,1,1,0,0,1,1,1,1,0,1,0,0,1,0,1,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,1,1,1,1,0,0,0,1,1,1,0,0,1,1,1,0,1,1,0,0,1,0,1,0,0,1,0,1,0,1,0,0,0,0,0,1,1,1,0,0,1,1,0,1,0,0,0,0,0,1,1,0,0,0,0,1,1,1,0,0,1,0,1,0,0,1,1,0,0,0,1,1,1,0,0,0]
number of clauses solved: 127 hex: 7f
number of atempts: 253617 hex: 3deb1
assignment of variables: [0,1,1,1,1,0,1,1,1,0,0,1,0,0,1,0,0,0,0,0,0,0,1,1,0,1,0,0,1,0,0,1,1,0,0,0,0,0,1,1,1,0,1,1,1,0,1,0,1,0,0,0,1,0,0,1,0,1,1,1,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,1,0,0,0,1,1,0,1,0,1,1,0,0,1,0,1,1,1,1,0,0,0,1,1,1,1,0,0,0,0,0,1,1,0,0,0,0,1,0,1,0,1,0,1,1,1,1,0,0,0,0,0,1]
number of clauses solved: 128 hex: 80
number of atempts: 2662974 hex: 28a23e
SATisfiable
real 23m3.189s
user 22m11.663s
sys 0m4.136s
loki@rurix 07:29:51 ~/CKUle/cse4401 $
}yzd e m2dyk 1V dqim