Skip to content

Instantly share code, notes, and snippets.

@marekyggdrasil marekyggdrasil/phi1.cnf

Last active Jul 13, 2020
Embed
What would you like to do?
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/
p cnf 3 3
1 -2 3 0
1 2 -3 0
-1 -2 3 0
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
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0
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
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
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
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
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
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
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
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
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
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
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
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
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
You can’t perform that action at this time.