Skip to content

Instantly share code, notes, and snippets.

@marekyggdrasil

marekyggdrasil/phi1.cnf

Last active July 13, 2020 15:06
Show Gist options
  • Save marekyggdrasil/e82e851522be9195239aba88e1f34c05 to your computer and use it in GitHub Desktop.
Save marekyggdrasil/e82e851522be9195239aba88e1f34c05 to your computer and use it in GitHub Desktop.
Download ZIP
CNF files for online tutorial covering the concept of SAT and boolean satisfiability in general, tutorial available under https://mareknarozniak.com/2020/07/13/satisfiability/
Raw
phi1.cnf
p cnf 3 3
1 -2 3 0
1 2 -3 0
-1 -2 3 0
Raw
phi1out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 3 |
c | Number of clauses: 3 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (886 /sec)
c propagations : 0 (0 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (nan %))
c polarity : 1 pos, 1 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000003 solve, 11 steps, 0.000016 simp, 42 steps, 3 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001129 s
s SATISFIABLE
v 1 -2 -3 0
Raw
phi2.cnf
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0
Raw
phi2out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 2 |
c | Number of clauses: 4 |
c | Parse time: 0.00 s |
c | Simplification time: 0.00 s |
c | |
c ===============================================================================
c Solved by simplification
c restarts : 0
c conflicts : 0 (0 /sec)
c decisions : 0 ( nan % random) (0 /sec)
c propagations : 0 (0 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 0 (partial: 0 savedD: 0 savedP: 0 (nan %))
c polarity : 2 pos, 2 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000000 solve, 10 steps, 0.000012 simp, 31 steps, 2 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001374 s
s UNSATISFIABLE
Raw
phi5.cnf
p cnf 11 22
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
Raw
phi5_1.cnf
p cnf 11 23
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
c
c forbid 0, 0, 1
c
1 2 -3 0
Raw
phi5_1out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 22 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (752 /sec)
c propagations : 2 (1505 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000003 solve, 111 steps, 0.000049 simp, 536 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001329 s
s SATISFIABLE
v -1 2 -3 4 -5 -6 7 -8 -9 10 11 0
Raw
phi5_2.cnf
p cnf 11 24
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
c
c forbid 0, 0, 1
c
1 2 -3 0
c
c forbid 0, 1, 0
c
1 -2 3 0
Raw
phi5_2out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 23 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (693 /sec)
c propagations : 2 (1386 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000003 solve, 117 steps, 0.000052 simp, 565 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001443 s
s SATISFIABLE
v 1 -2 -3 -4 5 6 -7 8 -9 10 11 0
Raw
phi5_3.cnf
p cnf 11 25
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
c
c forbid 0, 0, 1
c
1 2 -3 0
c
c forbid 0, 1, 0
c
1 -2 3 0
c
c forbid 1, 0, 0
c
-1 2 3 0
Raw
phi5_3out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 24 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (514 /sec)
c propagations : 2 (1029 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000004 solve, 116 steps, 0.000071 simp, 581 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001944 s
s SATISFIABLE
v 1 -2 3 -4 5 6 -7 8 9 10 11 0
Raw
phi5_4.cnf
p cnf 11 26
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
c
c forbid 0, 0, 1
c
1 2 -3 0
c
c forbid 0, 1, 0
c
1 -2 3 0
c
c forbid 1, 0, 0
c
-1 2 3 0
c
c forbid 1, 0, 1
c
-1 2 -3 0
Raw
phi5_4out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 25 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (751 /sec)
c propagations : 5 (3754 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000003 solve, 113 steps, 0.000046 simp, 537 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001332 s
s SATISFIABLE
v -1 2 3 4 -5 -6 7 -8 -9 10 11 0
Raw
phi5_5.cnf
p cnf 11 27
c
c N1
c
4 1 0
-4 -1 0
c
c N2
c
5 2 0
-5 -2 0
6 2 0
-6 -2 0
c
c A1
c
-4 -2 7 0
4 -7 0
2 -7 0
c
c A2
c
-1 -5 8 0
1 -8 0
5 -8 0
c
c A3
c
-6 -3 9 0
6 -9 0
3 -9 0
c
c R1
c
7 8 -10 0
-7 10 0
-8 10 0
c
c R2
c
10 9 -11 0
-10 11 0
-9 11 0
c
c enforce output to True
c
11 0
c
c forbid 0, 0, 1
c
1 2 -3 0
c
c forbid 0, 1, 0
c
1 -2 3 0
c
c forbid 1, 0, 0
c
-1 2 3 0
c
c forbid 1, 0, 1
c
-1 2 -3 0
c
c forbid 0, 1, 1
c
1 -2 -3 0
Raw
phi5_5out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 26 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c | Simplification time: 0.00 s |
c | |
c ===============================================================================
c Solved by simplification
c restarts : 0
c conflicts : 0 (0 /sec)
c decisions : 0 ( nan % random) (0 /sec)
c propagations : 3 (2211 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 0 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000000 solve, 118 steps, 0.000045 simp, 568 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001357 s
s UNSATISFIABLE
Raw
phi5out.txt
c This is MergeSAT (simp).
c ============================[ Problem Statistics ]=============================
c | |
c | Number of variables: 11 |
c | Number of clauses: 21 |
c | Parse time: 0.00 s |
c | Eliminated clauses: 0.00 Mb |
c Reduced to 0 vars, 0 cls (grow=0)
c No iterative elimination performed. (vars=0, c/v ratio=nan)
c | Simplification time: 0.00 s |
c | |
c ============================[ Search Statistics ]==============================
c | Conflicts | ORIGINAL | LEARNT | Progress |
c | | Vars Clauses Literals | Limit Clauses Lit/Cl | |
c ===============================================================================
c ===============================================================================
c restarts : 1
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (701 /sec)
c propagations : 1 (701 /sec)
c conflict literals : 0 ( nan % deleted)
c backtracks : 0 (NCB nan% , CB nan%)
c partial restarts : 1 (partial: 0 savedD: 0 savedP: 0 (0.00 %))
c polarity : 4 pos, 4 neg
c LCM : 0 runs, 0 Ctried, 0 Cshrinked, 0 Ldeleted, 0 Lrev-deleted
c Inprocessing : 0 subsumed, 0 dropped lits
c Stats: : 0.000003 solve, 92 steps, 0.000044 simp, 440 steps, 11 var, budget: 1
c Memory used : 0.10 MB
c CPU time : 0.001427 s
s SATISFIABLE
v -1 -2 3 4 5 6 -7 -8 9 -10 11 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment