Resolution proof compression by splitting
ಗಣಿತದ ತರ್ಕಶಾಸ್ತ್ರದಲ್ಲಿ, ವಿಭಜನೆಯ ಮೂಲಕ ಪ್ರೂಫ್ ಕಂಪ್ರೆಷನ್ ಎನ್ನುವುದು ರೆಸಲ್ಯೂಶನ್ ಪ್ರೂಫ್ಗಳ ಮೇಲೆ ಪ್ರಕ್ರಿಯೆಯ ನಂತರದ ಪ್ರಕ್ರಿಯೆಯಾಗಿ ಕಾರ್ಯನಿರ್ವಹಿಸುವ ಅಲ್ಗಾರಿದಮ್ ಆಗಿದೆ. ಸ್ಕಾಟ್ ಕಾಟನ್ ಅವರು "ರೆಸಲ್ಯೂಶನ್ ಪ್ರೂಫ್ ಅನ್ನು ಕಡಿಮೆ ಮಾಡಲು ಎರಡು ತಂತ್ರಗಳು" ಎಂಬ ತಮ್ಮ ಪ್ರಬಂಧದಲ್ಲಿ ಇದನ್ನು ಪ್ರಸ್ತಾಪಿಸಿದ್ದಾರೆ. ಸ್ಪ್ಲಿಟಿಂಗ್ ಅಲ್ಗಾರಿದಮ್ ಈ ಕೆಳಗಿನ ಅವಲೋಕನವನ್ನು ಆಧರಿಸಿದೆಃ ಅತೃಪ್ತಿಯ ಪುರಾವೆ ಮತ್ತು ವೇರಿಯೇಬಲ್ ಅನ್ನು ನೀಡಿದರೆ, ಪುರಾವೆಯನ್ನು ಪುರಾವೆ ಮತ್ತು ಪುರಾವೆಯಲ್ಲಿ ಮರು-ಜೋಡಿಸುವುದು (ವಿಭಜಿಸುವುದು) ಸುಲಭ ಮತ್ತು ಈ ಎರಡು ಪುರಾವೆಗಳ ಮರುಸಂಯೋಜನೆಯು (ಹೆಚ್ಚುವರಿ ರೆಸಲ್ಯೂಶನ್ ಹಂತದ ಮೂಲಕ) ಮೂಲಕ್ಕಿಂತ ಚಿಕ್ಕದಾದ ಪುರಾವೆಗೆ ಕಾರಣವಾಗಬಹುದು. ವೇರಿಯೇಬಲ್ ಅನ್ನು ಬಳಸಿಕೊಂಡು ಪುರಾವೆಯಲ್ಲಿ ಸ್ಪ್ಲಿಟಿಂಗ್ ಅನ್ನು ಅನ್ವಯಿಸುವುದರಿಂದ ವಿಭಿನ್ನ ವೇರಿಯೇಬಲ್ ಅನ್ನು ಬಳಸಿಕೊಂಡು ಅಲ್ಗಾರಿದಮ್ನ ನಂತರದ ಅಪ್ಲಿಕೇಶನ್ ಅನ್ನು ಅಮಾನ್ಯಗೊಳಿಸುವುದಿಲ್ಲ ಎಂಬುದನ್ನು ಗಮನಿಸಿ. ವಾಸ್ತವವಾಗಿ, ಕಾಟನ್ ಪ್ರಸ್ತಾಪಿಸಿದ ವಿಧಾನವು ಪುರಾವೆಗಳ ಸರಣಿಯನ್ನು ಉತ್ಪಾದಿಸುತ್ತದೆ, ಅಲ್ಲಿ ಪ್ರತಿ ಪುರಾವೆಯು ಸ್ಪ್ಲಿಟಿಂಗ್ ಅನ್ನು ಅನ್ವಯಿಸುವ ಪರಿಣಾಮವಾಗಿದೆ. ಅನುಕ್ರಮದ ನಿರ್ಮಾಣದ ಸಮಯದಲ್ಲಿ, ಒಂದು ಪುರಾವೆಯು ತುಂಬಾ ದೊಡ್ಡದಾಗಿದ್ದರೆ, ಅದನ್ನು ಅತ್ಯಂತ ಚಿಕ್ಕ ಪುರಾವೆ ಎಂದು ಹೊಂದಿಸಲಾಗುತ್ತದೆ. ಉತ್ತಮ ಸಂಕೋಚನ/ಸಮಯದ ಅನುಪಾತವನ್ನು ಸಾಧಿಸಲು, ವೇರಿಯೇಬಲ್ ಆಯ್ಕೆಗೆ ಹ್ಯೂರಿಸ್ಟಿಕ್ ಅಪೇಕ್ಷಣೀಯವಾಗಿದೆ. ಈ ಉದ್ದೇಶಕ್ಕಾಗಿ, ಕಾಟನ್ ರೆಸಲ್ಯೂಶನ್ ಹಂತದ "ಸೇರ್ಪಡೆ" ಯನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುತ್ತದೆ (ಪೂರ್ವವರ್ತಿಗಳು ಮತ್ತು ನಿವಾರಕಗಳೊಂದಿಗೆ): ನಂತರ, ಪ್ರತಿ ವೇರಿಯೇಬಲ್ಗೆ, ಈ ರೆಸಲ್ಯೂಶನ್ ಹಂತಗಳ ಸಂಖ್ಯೆಯೊಂದಿಗೆ ಪಿವೋಟ್ನೊಂದಿಗೆ ಎಲ್ಲಾ ರೆಸಲ್ಯೂಶನ್ ಹಂತಗಳ ಸಂಯೋಜನೆಯನ್ನು ಒಟ್ಟುಗೂಡಿಸಿ ಸ್ಕೋರ್ ಅನ್ನು ಲೆಕ್ಕಹಾಕಲಾಗುತ್ತದೆ. ಈ ರೀತಿ ಲೆಕ್ಕ ಹಾಕಿದ ಪ್ರತಿಯೊಂದು ಅಂಕವನ್ನು ಸೂಚಿಸುವ ಮೂಲಕ, ಪ್ರತಿ ವೇರಿಯೇಬಲ್ ಅನ್ನು ಅದರ ಅಂಕಕ್ಕೆ ಅನುಗುಣವಾದ ಸಂಭವನೀಯತೆಯೊಂದಿಗೆ ಆಯ್ಕೆ ಮಾಡಲಾಗುತ್ತದೆಃ ಅತೃಪ್ತಿಯ ಪುರಾವೆಯನ್ನು ಪುರಾವೆ ಮತ್ತು ಪುರಾವೆಯಲ್ಲಿ ವಿಭಜಿಸಲು, ಕಾಟನ್ ಈ ಕೆಳಗಿನವುಗಳನ್ನು ಪ್ರಸ್ತಾಪಿಸುತ್ತದೆಃ ಅಕ್ಷರಶಃ ಸೂಚಿಸೋಣ ಮತ್ತು ಷರತ್ತುಗಳ ಪರಿಹಾರವನ್ನು ಸೂಚಿಸೋಣ ಮತ್ತು ಎಲ್ಲಿ ಮತ್ತು ಎಲ್ಲಿ. ನಂತರ, ರೆಸಲ್ಯೂಶನ್ ಡ್ಯಾಗ್ನಲ್ಲಿರುವ ನೋಡ್ಗಳ ಮೇಲೆ ನಕ್ಷೆಯನ್ನು ವ್ಯಾಖ್ಯಾನಿಸಿಃ ಅಲ್ಲದೆ, ಖಾಲಿ ಷರತ್ತು ಆಗಿರಲಿ. ನಂತರ, ಮತ್ತು ಅನುಕ್ರಮವಾಗಿ ಗಣನೆಯ ಮೂಲಕ ಪಡೆಯಲಾಗುತ್ತದೆ. ಟಿಪ್ಪಣಿಗಳ ಪುರಾವೆ ಸಿದ್ಧಾಂತ