Resolution proof compression by splitting
ગાણિતિક તર્કશાસ્ત્રમાં, વિભાજન દ્વારા પ્રૂફ કમ્પ્રેશન એ એક અલ્ગોરિધમ છે જે રિઝોલ્યુશન પ્રૂફ પર પ્રક્રિયા પછીની પ્રક્રિયા તરીકે કાર્ય કરે છે. સ્કોટ કોટન દ્વારા તેમના પેપર "ટુ ટેક્નીક્સ ફોર મિનિમાઇઝિંગ રિઝોલ્યુશન પ્રૂફ" માં તેનો પ્રસ્તાવ મૂકવામાં આવ્યો હતો. સ્પ્લિટિંગ અલ્ગોરિધમ નીચેના નિરીક્ષણ પર આધારિત છેઃ અસંતોષકારકતા અને ચલનો પુરાવો જોતાં, સાબિતી અને સાબિતીમાં સાબિતીને ફરીથી ગોઠવવી (વિભાજિત કરવી) સરળ છે અને આ બે સાબિતીઓનું પુનઃસંયોજન (વધારાના રીઝોલ્યુશન પગલા દ્વારા) મૂળ કરતાં નાના સાબિતીમાં પરિણમી શકે છે. નોંધ લો કે વેરિયેબલનો ઉપયોગ કરીને સાબિતીમાં વિભાજન લાગુ કરવું એ અલગ વેરિયેબલનો ઉપયોગ કરીને અલ્ગોરિધમનો પછીનો ઉપયોગ અમાન્ય કરતું નથી. વાસ્તવમાં, કપાસ દ્વારા પ્રસ્તાવિત પદ્ધતિ સાબિતીઓનો ક્રમ પેદા કરે છે, જ્યાં દરેક સાબિતી સ્પ્લિટિંગ લાગુ કરવાનું પરિણામ છે. ક્રમના નિર્માણ દરમિયાન, જો સાબિતી ખૂબ મોટી હોય, તો તેને સૌથી નાનો સાબિતી તરીકે સેટ કરવામાં આવે છે. વધુ સારા સંકોચન/સમય ગુણોત્તર હાંસલ કરવા માટે, ચલ પસંદગી માટે સંશોધન ઇચ્છનીય છે. આ હેતુ માટે, કોટન રિઝોલ્યુશન પગલાની "એડિટિવિટી" ને વ્યાખ્યાયિત કરે છે (પૂર્વવર્તી અને રિઝોલ્વન્ટ સાથે): પછી, દરેક ચલ માટે, આ રિઝોલ્યુશન પગલાંની સંખ્યા સાથે પાઇવોટ સાથે તમામ રિઝોલ્યુશન પગલાંની એડિટિવિટીનો સરવાળો કરીને સ્કોરની ગણતરી કરવામાં આવે છે. આ રીતે ગણવામાં આવેલા દરેક ગુણાંકને સૂચવતા, દરેક ચલને તેના ગુણાંકના પ્રમાણસર સંભાવના સાથે પસંદ કરવામાં આવે છેઃ અસંતુષ્ટતાના સાબિતીને સાબિતી અને સાબિતીમાં વિભાજિત કરવા માટે, કપાસ નીચેની દરખાસ્ત કરે છેઃ ચાલો શાબ્દિક સૂચવીએ અને કલમોના નિરાકરણને સૂચવીએ અને ક્યાં અને ક્યાં. પછી, 'નોડ્સ' પરના નકશાને 'નોડ્સ' ના રિઝોલ્યુશન ડેગમાં વ્યાખ્યાયિત કરો, ઉપરાંત, ખાલી કલમને અંદર દો. પછી, અને અનુક્રમે અને ગણતરી દ્વારા મેળવવામાં આવે છે. નોંધો પુરાવો સિદ્ધાંત