Instantly share code, notes, and snippets.

# 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.
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/
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 p cnf 3 3 1 -2 3 0 1 2 -3 0 -1 -2 3 0
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 p cnf 2 4 1 2 0 1 -2 0 -1 2 0 -1 -2 0
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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