Nikolaj Bjørner and Mikoláš Janota
Microsoft Research
nbjorner@microsoft.com, mikolas.janota@gmail.com |
def sign(M,a): if M(a) return a else return
a
def level(j,a): return max level of bound variable in atom a of parity j
def strategy(M,j): return ![$\bigwedge_{M \neq null, a \in Atoms, level(j, a) < j} sign(M,a) $](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAArUAAAAzCAYAAACJ1vCtAAAACXBIWXMAAA7EAAAOxAGVKw4bAAAb2UlEQVR42u1dvXIbu5L+rHK4Aa2TbnKobENKfoAtD5ObbRVpFx/AZMi6ybCU3NRFJlsMSQUbsmQx2Jx07QMckbXRZprzBEdmcHNvMA2pBQEYYAb8Edlflcu2NBwCjUbjQ6PR/e7Xr18QCAQCgUAgEISj009rAK5m49FSpLE1GScA7mfj0cb13FmFL1h0+ulP+iKBQCAQCASCUyNbdQB/iiS2jkcAf3b6aSM6qSUimwCoARiKrAUCgUAgEJwgoV0B+CZe2u1iNh6tAXwFsHIR27Ke2jb7d4MGViAQCAQCgeAUCG0NwALAcjYejUQiOyG2cwAjAD9I/q/wvuS7u9r/W/RFAoFAIBAITovgdQFcIPdYbk6k23cAzpF7D0Pl1aLP2zCajUeDSGNzRxzNhovZeJS9IWI7oGiBHwAu9d+flRwMHT2Z1gKBQCAQnByhnQCYAEgB3JwQiU8AfC1D4snj2KQ/bQA6qUwit5NjSt/ZBHD5lggtw1fkUQKvwl/fhWY/cLD+S4p5EAgEAoFAcBoE7yfy+zUAMJ2NR70j728N+cWwbDYeXUZ654KIrToF38zGow8R2vmD3ts6tvEhmSXQPM1lYmo5oeUhB19kegsEAoFAcFKY0t9LAIMT6O81kfiYfU3wMhyhZosZDcANco8m99QujmgchtrfAAI9tVocyJwG9SHWzkIgEAgEAoHgEEGX4h+Qe2kvIr2zAWA1G4/edfrpAwB18b706TdxtSYRvgf2qw/HFPPM5PUkq1BPLXdbT8jlu2Y7i4aovUAgEAgEgiOE4kCTiO9MkHu5gZextaWySpGH95rCDLiXNjvCS3zKW36tfnAWKCgloA3LyXZrIb0CgUAgEAgExwIV8zqN+M4mnsMC1lVJLfKwgwF7t8L82AaDLtwBLCw2xFP7mf37O/v31PKMQCAQCAQCwZsHpZGqIb7Hk3tqeajAx5JtBHM6Hms8Lcea+t4NJbUvQg8YU96wAalJ2VyBQCAQCARHBsWBolUOUyGbLHa2avjBEJQ3l+J/+WWz+yMdFzUebW9SS8JR8bIbQ/DynYX8CgQCgUAgELx1KA60ivjORCPJpUkt5QvmxS+4g3F9xEUx/uD99a0oxtN4mWJJvuPZe9sS3RcIBAKB4DBBd2S6yFNxKvL0SKRqwmIVTZ9NkHsE6/SZSdkysYZ2PBLJGygS1umnNRshI0/njast5JQbALhC7rk8p35+c/XT0E4lp5geTx5Pi9l4lHX6qfpvLUCODQB1rT88nnZ5ADrXQO70TGgMHgHMeeU011g7sOTf4Rt+wL2vt/ovtRAEW9UxgUAgEAgE+yUXCfLiAV+I7P0+G48+UIqqHoCPVGTJ9NkuEdo2pfBcAhiaKjt5tKML4Cd954C1YQVg1emntU4/XQH42emnqYVo/lCfZW2ZsGcmRBoXs/Hokt7/O/36jj9bgITxnZhFphID4cw0IuiDG9Dxu6nN2HM8LenTijYGTTbWtU4/XdBY/6SxDsqiRfxTEeGrM4/G1NkOJXMM6MRCggUCgUAgEOyf0DaI4CyJ5C0NnrEEQEu/H0OfHQL4xCo4qYtN3RIkZ4L8ks8lu9iE2Xg0pd+t8Hzk/5vhNUPkFbKWGnHrdvppnSpOYTYeXXAPJvX3K3vWh0TVdcIZaSxMJDkoBIE2FBM+jocST0vj8ID8BH86G4+avPoXq272g7X3vMRXqXde+nhqOUGdO9gy/10SoRqGQCAQCASCeFAe2K+W308YkdTX8BvkHlpOgj9annURnQWRnA0R5I2BT4w0QmfyNHbx0pnGn18hjyPtFZAgReKLoAotbCvrQSlSq+470UYAlj7tJZ6WOKDyzi4dYzFkOleWgD8qefmQ2q6m8C5wYivpvQQCgUAgOACQ57WO/LL3xkF6N0RC5tpna9yjSmgZiJirDSkjXF8LyNaakdyl9p4WkbXMQLAB4J7HahpwbiCsLtQ18hQDTQtZXwW07Q7mk/FDiKfl3te247n7CARcfab+vkABG6xRugLZdnkt1ompmBKBQCAQCPaOJw9sp582TKGE5PEzrds9aE4tlReUrf1FhFaFLwB5KOPcs72mkMcveH2/p6G11+fdOoksIsGxPbUm4u3lqaUNwq2Fl+01npbapmQ8LSCqVxEIuNpsnBd5ap0XxAwTYskGXUIQBAKBQCA4PKw6/XQSkFf+1kB2OT/wcWANfUmw1q5lUXu07ARLDwfcRwuJtKGmkaeqpM8WT6u358ry+TqAL6asE3o8rcG7vm1CW9PG+q7gI80QnmnBE2kuSun1OVBpgTy9l9rBdQGMxH4IBAKBQLBXzDWy0UV+UQrIvaFLvMxzCkaM5gbi1GAkclNAdOp46T0s8tJyorMoag/CPZOtQNIX21Nri6f1Tes1gT0u+kU87R70jHvwNx7y5WNRtr1/KXmdFeyUeOiB72DyHdgXsSMCgUDwdtHppy1biqc30v6FVLrMyRKASwsxawBIAfxJBLQI3Evrk86Lp/nMPDypSSDp9I4h1TI6zT3F9xh5OJoF5FvPZMDb3yVOtq4qiy3B24Ove9hjfPmZZ8MmARNnzQak4TlBjnUxaJTJ3yc4Cd3oSniO4A3oaQpWevONooc8J2n31MdzNh6tKadrjwidTnBr8PN0KlluYpNORrIBf09jSB5ZTrBDj7tj2eykQA788lRdI4G9gktwe4un1Uiqz/fHaqtK+bZ57znw3wO/YEq7PvWeUQUh/TL8OKPEvWXex3PfgU3MD1sY4ztEzGu3T3KO5woy5zSxL3Xj4fucEIV0QovCY4CnQLBjfT71/hIJvEaenH9T8nuvkR9p7022dJx7iTyO9NG3itQBjV10GfILYeR46rE1u267SEbPtxi58w1L5ETnoaDPSQjpLOHt6zE5+OqC0v/zSGNaRL4zjeCrft24Npja5f6dx9Nq4+zz/bG8yk8xz2cOpX36ohIG7dakQCUn3zsAH2jybNikq5VQpgnr/IYEerENQkseDlWe760jYwS95piQvs+dOqHqmgyA705YvLw70+eT7S8RiwmK0y4VbepbRMr2CjruHiD32Dbe0NhVlmGnn6YUgtGyyYY8f20bObGRQrgzItjITtFcCyU6nzV5FdnfuomQk21NCkhmDLubePSLE/8LxsseC+buvuNp6xZiXjR2G94vKtoQEjL0FPN8Fqq0ngZkzTpUr2pEyKiea0p4FTixdQF9p2oq0T2p7Pbf/BgWy9l4tKGd/do1WXyfO3Fwo/uxxOdvaE52RZTb1ecT7+8EWq7SElDrwLcDkYOSwc2ON7JJhTWwkgxZ+EhSRPi0sc4ca5taS1+k+aTfTQpIIVCcXD+0JG0ICe45CPA1Xp/i6u0/j6ASRfG0uryUE+/aUcCg7IZgGxtoL1KrZWm4N4xTyJxR78neFygtKhi1CZ4DyL9EWDgSAJ9o11pHuJdL7UR/0v+3GWui+v2W49BcxmYZ6bm9gxabLzSBbDplrXwT+F1D5OEGqYc3xIaWbBh2rs8n1V92ytSsSCLbByiDr8jDELqGKkyxbUsLz2EfU5Q4tYwgwy8aQS5yxgB5eJ/tWe4V1Yl2F/ZwhLWydy47Sva4ETgvlV5vAi6gZYaj8S7yi3QmPFSw2aY2FJ3gcvnXaSPmc+rLnX2LCrqbIC9gsQnU1zXL3FD02Z5DN7vE93zxVMb4rEBpq+zS51oDqxiHOvJqJtwDfBnw+QkpRFHuuxiGrE79HeyjNN2W0fCcLI2qk2oXZJbiq1eMZC4tf24jENoGgISO+bIyBlI7bbiHYFf6fGr9vYZfsZ03B7aGDLdoW1pU7155AtseHrZt4ZHIxRLuqk5q3FFAvptMlnPD521yXRjIswl3IaRM8/YVbdZ47K2eoqwLd35bZW9rVUK/lA0v8kBr7VCbgaL+RYmnJd1dAPhpC1nxJOS1Ajmk7Ed/aP14DDzlVuO6MF0U44o/qWA8sk4/XZMhrbkCzz13NksmsASe4QdciTr9tMd2adsinBPaMR5Vfl5OqFyTxfe5PfdFHclltODs4uIID/DPaBLWOv20FqCLakFZH+GG6SD1+QTnb5cWo8kRi2MOIO3001bMua95ZndpW1BAEs9n41HTQz9S5NWfXPMh0/7mjqPvNlI4G4+mtP42kDvOpgbC+QMvj/d95qX37fnZeLRhXsQH7buHcDjKNA9kghIOPx6e4Wn3NzQXN/A79fX2yhfocF1bt0L7+pWcRYmpn2ye8Cp1XG96Id+phfbcvzcIPaaxv2XegR7KXxrjMSh/aF6HIgzYhN7qcSMZhsRjR/wW0fSUXXObMo5IaEcFaVFif+eSberWTBfrCE9bcyrH5Yegz6c6f78fsSxuicA1ESH7iEZm1wdCZjmZvCDv2wDaxW9as3rIw5oGHs6YCcmOX9YeAriajUdFp6dtWscnnX6azcajJb3jM57Txg0RdnmTk3UfnZ0iP0m9YP1XFyKLTiaUk+6jr97Q++tEmPmJ9YrC0R5hv4yf0fcZL2tql94+4qXns04bVOWp9w0leJXirdNPkxAuSBuAAY3lXaeftmlDoS7OXyHPvrLp9NM2rWsJgDW1OQnMbqUcnNlsPHqV0qurDX5VTPF8HPG5AqlN8By/8+KGnEsRWdiBfvSwrePGCXnRQnYZE0ZWJsqoUHu7tPuq0Q52SYanKAC7QTssZXR6NqWkpOoJitP2JJ6yS7YlY2aAG2zS9+hUoIWCTB30+V0TWlXOkBt8frPVSmppbEzHPykRZcAjHZ1Bl5TxurUtYlX0Ul1qoM/X2Lwd+B5pMwOo2nCO/AhwGMmzGqynLPVRA8+psTYkn2nZuci8VCrV1iZmG0rM33XJFF7qln6NORTmhzL/tUV3o3n5YpDZZlXd3IYMZ+PRoNNPb0l2w04/Vd7QR5LhAp5ZLlh6tBsAf9I75h6EVh2pXxCZG5IuP5L9+J3Zw5DN5kLxA8/292jsW0Sg7mkT4kOglZOuEWAvbPOtzryUbQtJXhJRm1ts+srx9fppS9uHiNNGQxH/DM/e4lCdG3X66ZJ0eUU6l5Gd4inVmqQPvU4/vabxCI3lV8/PAeDdr1+/uKB4DtdmjMWj6jtJMR4otZf62a+i95EBbCryQv9XCvbBZwIExs78HcA/APw7gP+1DLTuhh8yo6NutPdoYO9oAee5BB9IyawElBbRO+p7Rjv0uqnP1D91ce7CRji05y4d+Qu9niupR3e6N4H1NSPD5vQ0kCw2PgY4YrsX1K61pptKF50Em+kgv738waZThs931WaLFq41k90PWlQuNe9NKb2cjUcf2Jg8Lcb6M54L+x0RlqlhkehVsU1l9JTJYa4ReCXHgU4qGaFtu+YiGyPofa7ahsD526CFch56QYl0pkF93ZDeJxHXkcrz3zAvE5fdK5hTA0ZmB5H6uFUZHjrYvHfOgz22L8iOHcmYTACsDm0sDOt6Xdm2M23AGsz7E2sS8d1CGU+tKaebMkINx6I10MhCk7uoPQT1kxYC3z//oI/+j+0ZQ9B1l7VRee8GtEC1uSKR4V3TrsnlYbhTiyjzcAHmGGSeI85l2K+4lyPCc2U2Ri0ydCPtO7hHMSvw8uw0b7CjnKGxWoxtI0T6qtJ/rdXPPAjthOQzn41HL8gM/fsrff9dDL2kRfmOjMtceyajZxIPwnlDZF83pOq4rWp4j7eeUu7KFZ4vf/K5pT7/3eJduMPLY03bXPwORx7Mim0oM3//CNTzFEBjNh41mU5mzEO09/lvgHMNsc1nWkAn5Fxo0ryKQWi3KsM3gn2no/LxNC997NgR4RwHXECKlTx+ytjBww+qVBBz4Tsjtq2Siq678FV6EFuez6GBvITGI17C/3b63wH8DcB/APinY1IsNcLD2/KRkZxmweJz7tjpZpo3zpYHjhuRIpm0Iz8XulNsID9aNO0Wl56GsB15s+bjDeyZvMLahQVfHQvSXyKYXdIH26Ko3vUU0F9SL5WOpeT5cpHtotOPz/TMX4bfqbZUDW0J0dM70r+5wwuY4HUSeu+5SHLvUb+yWG0o0V8emhKi59d4Pj4O1etdzX8dDy5baticqljPKGEGu5ThG4Kvk2WfUJuoNk4jHj/BYacm7bFxgU5qKxVccHmaKLYiUcY+MEaIx9OCeRJapl027aD06hQ1BKbvYd4ln53C38iD8t8lJgg0j4Hr9mndQVCVgR4axtQWa+Yrk73E02rVt4YF31nkga9jt2mw7gqMgbp04Osp8tZfkltqmNcucs1v9JbVy5FjMaqzfvsQq2Gnn/6GPO53Te0ddPrptwiZH7z0lIipenZgmPcq/nFpIJtBc5Fi2V7Jp2IbQuelupzxGGqfDX2qbAsiz//gTRbJ/oaR2cGWNsVbk+GBeNIGtCa7wqx4/P3BVuGcjUfzTj/NAHQ7/XRwzFloaP5lB97HLrRsU+9Z4+vMOMRO7M6PiLzTNWj5aXVC8Gony8IO9GO4K8NnY/YtC03hpcUK8ktsE4eCOW+FGjwZn23v9K2XHfu5QAzZzt32Tl9vcx35jdBfJdrhjGN2kKEVI41OT41HQvIn8uPRhGsPucFU5aikXqLgmZDk6HM27inyS3FqfIcRLuKE6OmL6kPaWGa0uf5kmo+OuXjnaJdJPqXbUKK/wdWSLJdYuE4sD2T+m+Y0J/K28a+RnL9uqzrklmW4T1JUw8vUWX84Lj2pebE+5PhNphcLsrMDHC+ucSDVAC36pdIPvjiJVJ7aL9qiso3dzdPuMyA3Z8MyoXlpPp4BwVZ1oxmwqIYIVZGXqjFPfNG3Gc4vIaSc73wtnnFfouFbsjC0tGGIXL5X9brRIrZGfoM1FFkAoVVHiUUpSQbMC1WU1isJ3JC1POSmb/ayknrJ06nY9EjNj3sPW5F1+mmTCHJda0vS6adVL5CE6Kl6dloleb42F6eO7/q+hTaE9PexLLm1fGdVL0/M+a+jMNSCbmarS2ErOnEc7Kj0eSwZ7hOJxRml20uV+WONsCpSewGdqiyRe2u/HaO3VlV2O9CqgHzT+yrblCK13SJvSwTM2WL7KvmyYxe+sCx8nPhmegybZXKVybzgwn8C+D/k+dWKnn10KL+Pt6EbOD5FcXSx885GzfupyXPlmHi+3owMQH0HRTFu4Jd2jfepiNR6y1aT24PnmNlIq8/3+jzzOUR3ySt3QQveFemyirUdolq6wTJ6+lBRJ3xiWq/hDld52EF/HzTCt0sZb3v+6/iN/v6rQBenAKYGcjvccnz+MeRR5m1/YRO1/LQ17DDNYiT0aL6oIgLHRGiV57x9wG1UevPKZp5pFxiyLQZoTwxG3menZ1vs1c8/Ku+YY1IEl8Ok7AcPBX/+FcC/eTz3AHfJOae3QRuj7+znd44uXNl2xxrR4OXphoY0Zq/aVvG5Msh8vRmdfprQAqRjAaARqT02nWkxUhbSp4+eHo+FvvAbdODR5RnRDJfSx0EFL1iR7rZgODHQ2636wucIZXhYkofyMhLhCtHTTYH++cI5Fx1hVjHaUKa/v8WW8QHMfx31ELnOxqMpJYTv0WcXnX662uIt+DcfT0tjckGb0F6nnz7Qn5/Ic9y2kR9vf3hjhFbduWkj99YeWyaEIXZ3IlFmnVV3RnqmNr7Hy9CDyRaVYElJj2vwCEFQsWAOgnCP54s2NzYvh6ZwIbveT7DfPv0XAP9F7/OVmTEuzDPmTY3RkhnvoktGNZ206oso/06VVJ8bF1PbqjxnGZtHS0wi98Znjt2yThZ6MIcYqCwcW4mD8im1aNBffYEt8ljdG4zPQl9I2DwrMlxKp6Zl9FLbbBXp7tREdBnUDf86DCFQpA+bIhLi0qkSenpP5KLuMf4T5InFXQvBH44N/8ChJ6XaULK/QIVb9yHe0x3Pf5t9DFq4medWFV5YUDn4aJfIjiGeViN/R+XJZH2bd/rpCHms++UBZ2wI7dfBjhcLV5naQrne4+Xxy7YDtKfEsOERh9ItWMBWbEc7ciwmpeJp6X1rx+IBUJLsSDtyV/sStvC/2E0VeDfqMMfHLQxekM94Hbt2rsmj6nNchk8J56mMninuV4Ws1PG61viQLb6cLCSmOCAiewPkt+pvt7ALvYNnRSPWnkJSyxbfjZawv0WbPtOc/Ub60TQtiiT7Lul3O4JeuuL+GgbdNR21qws5AwcBqsFxRO+hU6F6OiA70wQwKjCyjw6dumeE3dTmjSMjTJU2BPWX1bdvRLBnWYHTYqfz34ArRrpKERoA8y2R22OIpz0JUEaWGq2pFyKRreMHrbNW4n1GMYZtFOeXjKIAtGu7cHmmKBH1EPlt9cRyVJaxiT+wvCfBcyxqRj+rdHxJnjOVBD2GvHxqrSsPyiMz6FlBajTlieupPlP/F3iuMAU81/AeQEubw9OaMdmVfs7Sbzh28l+RH4kOWR8a1AcwAvQbk8s3h/6NiOT9MN38L6MLnX7aovjYBMC5j35RH/gRaYPeU7dsrjbIE34rGaREDD8V9DPlx/nUXlWQYUqJ4zcV9PIjIx82rA0bwqWBAA6pn486YSNZqQpj67I6Faqn9F0j5CdLqWHsh0Q4l4aMK6a+XfMxpnf2XCSsShtKzss5swlV7JlvDP7O5r/mCa0hwqXo2Xg0p7CENr0zRljCMcTTnhKx7QGYqEqMgu2A7N+yaNP6okzuATR6AXu1rAtDoPmfMKSzoZgdl1EunTyb2lgnQxajzypJ/ifXgk0xiAmea20PPN7doAXsij63UZ4EWlwn9LvM5mEwPPfNkpbF6zmtbapMK2zyZBWmnqrd8bYqYqAW5CK5MK9WAwFlNS3tX1mM3LuC8Xbl+eoZyq1y2T4W7VTZ51p4jgHkpGXicZGtUC/ZM5cFJZZvmO5ObDInIjAweDTVxZzMY0ycOhWqp6xdPc2DmQFYBJRlVfk6P7O5eBvw+VJtKDEvlQe1HZhPXLe97UOc/+wzw7J99JhzyotcynPrK0OBQHDgpPYN7BRUbWoxNnHlujJV3tryd06IkG2QeyNXtOibEs9vjiVeSnRK4CG7Xyj2PtsItMqg8CEgDd5Ox4pOVuqz8ejDltcKTm698tyWlaFAIMhxJiIIgjEvmqCS8a8hrIJRFJCnU93MVSVGF0Ru9T8P28yaIDgOnToiqHCH0BAdFeoSmtf5cYe6kYBOabZsX3hYAuB/WSpYhgKB4BnvRQTexjClXbd4f+LiM/aUtoa8rwO1wGlZITg2ssCITp0K6PKL8jQ2DbawTiRNv3D5qg77AY6VckxMdyTLOQyxu5FlKBAIhNQGEdqnpO+HmrvtDWNwKBsFCTEQnRK8IFeLTj9NDDGhqux5Q5FeisWtI7xk+M7Gioh6A4dxSz2mDAUCAUHCD/x398oAC+ItMhPklzvECyoQnTogEJHtIc/BqZ9eXDFipk6xVFaLi0McKwqlUPchDmHzGkWGAoFASG0ZxEzhJcDT8dv5W6skIxCdOiFiO0WeImulEdtPyC8/DemmfpPIYvMQx4plPOkd0H2IyjIUCASvIdkPPI2iEFqBQHCi9q8F4ItnUYNDbP8d8thVueArEBw5/h+KPOwhIhTV6wAAAABJRU5ErkJggg==)
def tailv(j): return ![$x_{j-1},x_j,x_{j+1},\ldots$](data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAATQAAAAeCAYAAACiweJ7AAAACXBIWXMAAA7EAAAOxAGVKw4bAAAE5UlEQVR42u1d3VHbQBD+YFyAQjowHRg6wHSAM6MCgh/1Jo8rYHxv9yhTwA1xOrBLADqI0gFxB+RBK3IRsixbknXS7jfjGQHnk/a+T3e7ez+cvb+/Iws/CMcAZgCu6VcxgMhotbTKDAEsAIwAXOSVEdQLbryIDgWH4jxHRBEJZGG0+mK0+gLgCUDkB+GKyowAvJBwLqnMM5UJpVkbeblZ8SI6FByDM9tDIxENjVa3OQL7BWAIYEpCuzFavVrfu6eir0arK2na2l9uNryIDgWVPTRy78d5IrLcfQCIAPxIRUT4llNOUF/YxYYX0aGgCgbW9QrApKDs0LpeZP72AGBO7v73I0Q8ou8/ZATqwgs2AnBhtNq09AjceBEduqfBbnVofhDeAXjb02CpkGKj1X+jn9FKAVAVRZzWP3FMSC8ANvQ59f1Z8dIHe/0g9IxW275osKseWlxEIDVqiiYa9dUaYV3pyKZWPqYtcOOlD/b+9oNwVnWW1SENdq9DK+Fej63rdd0PYbRywivzg/AFyfR/TC/MK/3cCrjx0hN7Pfr0QoNd9dD24bbhkdEV3NjhAi0PcFlMXHjhZG/XNOgUzkuWG1t5i21fG6ODtrHghZO9THhsr0OjaXROXkAnwI0X0aGgrpDTdvPXBYIbAvDKTHfTbNbcyjXMjFY/hY6jwy8OvIgOBbWEnGVHRnvKu0hECySzNzdGq0skyc9VZgQWCC+iQ8HhHpofhB6ARxLM0mg1y4x2o315C5piHu4b3Wh/3SizCjxdSzTpYyhBL8jzobmRrvLCzd4+a7Cgrk9rANuqJ1vXOZLV1nfkdmc39E6t66LGeMSeldkk2Dk+rzMaoqegfYdrAH8ovDkEneOFm70MNLirrl9+EN63XU9eXYMMkT8zo+I9iSnaRThNK8clcg9jJFtKtjtCiXXPhHSXabNHu31LoFO8cLCXnqUMvpYo+9b0jGYNnBTVtQCwbKueXXUNKOeQuvlTy4WLAEyMVhs/CK8A3PtBuEhDASqzIBHtXZCYJ7SyK7/9IFxncihV8GFnw8iK1fODcHzAfjzneeFkrx+Ef1B+wWyY42Xm1TlpeBKiKidFdcU1PVNco33xwGi19IPwDcCcSHtDsjr5No1vjVZT6lTSMkCyAXhWccNs2XVFCxK8VwPBz6fw0OgFXJJ3EdO9vQO+3wVeONl7UzIsXZHHsc+z3Ta92bwqJzl1KeqoYxyx+b/OenbVdZZ3Yu0Jw7J1dlR2LGxcUV5nU3CcTdm6IgAvXThJtQ5euNlr1fVOHawSDZ4e5y3fv5f5sx24QHfO6KqDF272igY5d2gnODnBxZfm2fWHrJEXbvaKBpl7aGz2IdJL0xU7K/PCzV7RoHRowL+tLBsHyfdIAOnofX3AlH0e5nDkrLcT8cLNXtGgIxi0eO9r1/IWmX+yYcNDsnDvIzQpm6BNRenKmW9N88LNXtGgdGgfG4hdGxlphmtao50e9p+R75JXUIkXbvaKBiXkTHHHIW+BZP3czLV//NIgL9zsFQ1y8tBoBJwCeMo0aDoCRX1uXBfX1jXJCzd7C7AVDfYz5IyQzCKNQMlX2ow6pFFRQdAGuPFySnuvuHhDHEPOa3sEpGNbIiQJzUtp/tbAjZeT2SudWbtodOsTza48Ikm8XiBZ1BfJqaCth2CseBEd8sFfqsdKX8yw7pEAAAAASUVORK5CYII=)
j = 1
M = null
while True:
if
strategy(M, j) is unsat:
if j == 1:
return F is unsat
if j == 2:
return F is sat
C = Core(
, strategy(M, j))
J = Mbp(tailv(j), C)
j = index of max variable in J
of same parity as j
=
J
M = null
else:
M = current model
j = j + 1
Note: core for is implicant of
.
Extends to Quantifier Elimination.
Enumerate literals that imply
by tracking clauses asserted at level 2.
Our base strategy uses limited look-ahead.
It is possible to formulate stronger strategies (based on models)
|
|