Skip to content

Instantly share code, notes, and snippets.

@marekyggdrasil
Last active July 13, 2020 15:06
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save marekyggdrasil/e82e851522be9195239aba88e1f34c05 to your computer and use it in GitHub Desktop.
Save marekyggdrasil/e82e851522be9195239aba88e1f34c05 to your computer and use it in GitHub Desktop.
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