Home

Downloads

Examples

Documents

Psyche

the Proof-Search factorY for Collaborative HEuristics

Examples of Psyche runs on standard benchmarks

These examples were run with Psyche 1.4, on a computer equipped with an Intel i686 3GHz processor with 2Gb of RAM, running Linux 32bits. We used its DPLL_WL plugin that emulates a basic DPLL implementation, using watched literals to select clauses and literals, and a memoisation table to perform clause learning.

QF_LRA (SMTLib)

These runs have been obtained with a decision procedure for Linear Rational Arithmetic that is not incremental (the procedure has no memory from one call to the next). Better results are expected with incrementality.

Our first example is the unsatisfiability of the three clauses
x>0, not(x+y>0), (y>0 or x=-1)
This is expressed in this SMTLib2 input file.
Running the command
psyche -latex -gplugin dpll_wl DPLLTh.smt2
produces latex source which, when compiled, produces this proof-tree.

The other instances are taken from http://www.smt-lib.org/.

bad_echos_ascend.baseUNSAT3.992249 sec
bad_echos_ascend.inductionUNSAT1.252078 sec
bignum_lra1SAT0.004 sec
bignum_lra2UNSAT0.088004 sec
Carpark2-ausgabe-1UNSAT0.32802 sec
Carpark2-ausgabe-2UNSAT4.572286 sec
Carpark2-ausgabe-3UNSAT26.221639 sec
Carpark2-ausgabe-4UNSAT53.479342 sec
Carpark2-t1-1UNSAT0.608037 sec
Carpark2-t1-2UNSAT5.248328 sec
Carpark2-t1-3UNSAT23.165448 sec
Carpark2-t1-4SAT36.138258 sec
frame_prop.baseUNSAT7.768485 sec
frame_prop.inductionUNSAT1.028064 sec
gasburner-prop3-10UNSAT10.840678 sec
gasburner-prop3-11UNSAT11.496718 sec
gasburner-prop3-12UNSAT24.189511 sec
gasburner-prop3-13UNSAT40.102506 sec
gasburner-prop3-14UNSAT29.481843 sec
gasburner-prop3-15UNSAT43.902744 sec
gasburner-prop3-16UNSAT60.703794 sec
gasburner-prop3-17UNSAT72.620539 sec
gasburner-prop3-18UNSAT109.902868 sec
gasburner-prop3-19UNSAT139.084692 sec
gasburner-prop3-1UNSAT0.008 sec
gasburner-prop3-20UNSAT161.666103 sec
gasburner-prop3-2UNSAT0.032002 sec
gasburner-prop3-3UNSAT0.124007 sec
gasburner-prop3-4UNSAT0.300018 sec
gasburner-prop3-5UNSAT0.636039 sec
gasburner-prop3-6UNSAT1.020064 sec
gasburner-prop3-7UNSAT2.724171 sec
gasburner-prop3-8UNSAT3.340208 sec
gasburner-prop3-9UNSAT5.836365 sec
good_frame_update.baseUNSAT185.28358 sec
good_frame_update.inductionUNSAT37.726358 sec
pursuit-safety-10UNSAT945.219072 sec
pursuit-safety-1UNSAT0.020001 sec
pursuit-safety-2UNSAT0.380024 sec
pursuit-safety-3UNSAT1.876117 sec
pursuit-safety-4UNSAT7.964498 sec
pursuit-safety-5UNSAT18.649165 sec
pursuit-safety-6UNSAT41.838615 sec
pursuit-safety-7UNSAT101.914369 sec
pursuit-safety-8UNSAT366.406899 sec
pursuit-safety-9UNSAT523.640726 sec
tgc_io-nosafe-1UNSAT0.040002 sec
tgc_io-nosafe-2UNSAT0.560035 sec
tgc_io-nosafe-3UNSAT4.524282 sec
tgc_io-nosafe-4UNSAT16.725045 sec
tgc_io-nosafe-5UNSAT71.232451 sec
tgc_io-safe-1UNSAT0.044003 sec
tgc_io-safe-2UNSAT0.508032 sec
tgc_io-safe-3UNSAT4.776299 sec
tgc_io-safe-4UNSAT14.012876 sec
tgc_io-safe-5UNSAT71.608475 sec
uart-5.base.cvcUNSAT106.342646 sec
uart-5.induction.cvcSAT13.868867 sec
windowreal-no_t_deadlock-1UNSAT0.016001 sec
windowreal-no_t_deadlock-2UNSAT0.056003 sec
windowreal-no_t_deadlock-3UNSAT0.15601 sec
windowreal-no_t_deadlock-4UNSAT0.64404 sec
windowreal-safe-1UNSAT0.028002 sec
windowreal-safe2-1UNSAT0.032002 sec
windowreal-safe2-2UNSAT0.172011 sec
windowreal-safe2-3SAT1.456091 sec
windowreal-safe2-4SAT2.900181 sec
windowreal-safe-2UNSAT0.180012 sec
windowreal-safe-3SAT1.300081 sec
windowreal-safe-4SAT2.460153 sec

DIMACS

These runs have been obtained with a decision procedure for the empty theory (closing a branch requires finding a literal and its negation in the sequent). The instances are taken from http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html.
Instance#variables#clausesstatusPsyche
aim-100-1_6-no-1100160UNSAT0.536033 sec
aim-100-1_6-no-2100160UNSAT0.472029 sec
aim-100-1_6-no-3100160UNSAT0.788049 sec
aim-100-1_6-no-4100160UNSAT0.592037 sec
aim-100-1_6-yes1-1100160SAT1.348084 sec
aim-100-1_6-yes1-2100160SAT0.192011 sec
aim-100-1_6-yes1-3100160SAT0.444027 sec
aim-100-1_6-yes1-4100160SAT2.348146 sec
aim-100-2_0-no-1100200UNSAT1.072066 sec
aim-100-2_0-no-2100200UNSAT0.724045 sec
aim-100-2_0-no-3100200UNSAT0.48803 sec
aim-100-2_0-no-4100200UNSAT0.800049 sec
aim-100-2_0-yes1-1100200SAT1.168072 sec
aim-100-2_0-yes1-2100200SAT0.904056 sec
aim-100-2_0-yes1-3100200SAT1.252078 sec
aim-100-2_0-yes1-4100200SAT1.552097 sec
aim-100-3_4-yes1-1100340SAT1.116069 sec
aim-100-3_4-yes1-2100340SAT1.140071 sec
aim-100-3_4-yes1-3100340SAT1.552097 sec
aim-100-3_4-yes1-4100340SAT2.104132 sec
aim-100-6_0-yes1-1100600SAT0.79605 sec
aim-100-6_0-yes1-2100600SAT1.564097 sec
aim-100-6_0-yes1-3100600SAT2.08413 sec
aim-100-6_0-yes1-4100600SAT1.340084 sec
aim-200-1_6-no-1200320UNSAT6.752422 sec
aim-200-1_6-no-2200320UNSAT6.844428 sec
aim-200-1_6-no-3200320UNSAT7.128445 sec
aim-200-1_6-no-4200320UNSAT1.668104 sec
aim-200-1_6-yes1-1200320SAT5.496343 sec
aim-200-1_6-yes1-2200320SAT4.8043 sec
aim-200-1_6-yes1-3200320SAT3.944246 sec
aim-200-1_6-yes1-4200320SAT5.680355 sec
aim-200-2_0-no-1200400UNSAT5.176323 sec
aim-200-2_0-no-2200400UNSAT1.544096 sec
aim-200-2_0-no-3200400UNSAT2.744171 sec
aim-200-2_0-no-4200400UNSAT12.916807 sec
aim-200-2_0-yes1-1200400SAT10.280643 sec
aim-200-2_0-yes1-2200400SAT23.489468 sec
aim-200-2_0-yes1-3200400SAT3.532221 sec
aim-200-2_0-yes1-4200400SAT24.80155 sec
aim-200-3_4-yes1-1200680SAT9.988624 sec
aim-200-3_4-yes1-2200680SAT31.709981 sec
aim-200-3_4-yes1-3200680SAT93.345834 sec
aim-200-3_4-yes1-4200680SAT319.84399 sec
aim-200-6_0-yes1-12001200SAT8.872554 sec
aim-200-6_0-yes1-22001200SAT5.696356 sec
aim-200-6_0-yes1-32001200SAT57.075567 sec
aim-200-6_0-yes1-42001200SAT11.460716 sec
aim-50-1_6-no-15080UNSAT0.072004 sec
aim-50-1_6-no-25080UNSAT0.096005 sec
aim-50-1_6-no-35080UNSAT0.092005 sec
aim-50-1_6-no-45080UNSAT0.076004 sec
aim-50-1_6-yes1-15080SAT0.228013 sec
aim-50-1_6-yes1-25080SAT0.044002 sec
aim-50-1_6-yes1-35080SAT0.16801 sec
aim-50-1_6-yes1-45080SAT0.096005 sec
aim-50-2_0-no-150100UNSAT0.140008 sec
aim-50-2_0-no-250100UNSAT0.092005 sec
aim-50-2_0-no-350100UNSAT0.072004 sec
aim-50-2_0-no-450100UNSAT0.036002 sec
aim-50-2_0-yes1-150100SAT0.236015 sec
aim-50-2_0-yes1-250100SAT0.088005 sec
aim-50-2_0-yes1-350100SAT0.108007 sec
aim-50-2_0-yes1-450100SAT0.308019 sec
aim-50-3_4-yes1-150170SAT0.81205 sec
aim-50-3_4-yes1-250170SAT0.824051 sec
aim-50-3_4-yes1-350170SAT0.64004 sec
aim-50-3_4-yes1-450170SAT0.444027 sec
aim-50-6_0-yes1-150300SAT0.184011 sec
aim-50-6_0-yes1-250300SAT0.212013 sec
aim-50-6_0-yes1-350300SAT0.236014 sec
aim-50-6_0-yes1-450300SAT0.220014 sec
ii8a166186SAT0.108006 sec
ii8a2180800SAT1.256078 sec
par8-1-c64254SAT0.380024 sec
par8-13501149SAT7.04044 sec
par8-2-c68270SAT0.664041 sec
par8-23501157SAT12.556785 sec
par8-3-c75298SAT0.48803 sec
par8-33501171SAT11.712732 sec
par8-4-c67266SAT0.176011 sec
par8-43501155SAT9.804612 sec
par8-5-c75298SAT0.212013 sec
par8-53501171SAT10.264641 sec
ssa0432-0034351027UNSAT348.889805 sec
ii32b12281374SAT4.272266 sec
ii32c12251280SAT3.884243 sec
ii32c22492182SAT10.872679 sec
ii32d13322703SAT67.824239 sec
ii32e12221186SAT3.84424 sec
ii8a32641552SAT3.896243 sec
ii8a43962798SAT13.472843 sec
ii8b13362068SAT6.556409 sec
ii8b25764088SAT26.481655 sec
ii8c15103065SAT18.261141 sec
ii8d15303207SAT17.825114 sec
ii8e15203136SAT17.381087 sec
bf2670-00113933434UNSAT245.12732 sec
dubois2060160UNSAT2.528157 sec
dubois2163168UNSAT4.088255 sec
dubois2266176UNSAT4.788299 sec
dubois2369184UNSAT5.096318 sec
dubois2472192UNSAT7.272454 sec
dubois2575200UNSAT7.728483 sec
dubois2678208UNSAT7.540471 sec
dubois2781216UNSAT11.68473 sec
dubois2884224UNSAT10.524657 sec
dubois2987232UNSAT15.120944 sec
dubois3090240UNSAT17.145071 sec
dubois50150400UNSAT135.772485 sec
hole642133UNSAT9.628602 sec
hole756204UNSAT92.781798 sec
jnh10100850UNSAT0.988062 sec
jnh11100850UNSAT11.388711 sec
jnh12100850SAT2.140134 sec
jnh13100850UNSAT1.548097 sec
jnh14100850UNSAT3.556222 sec
jnh15100850UNSAT4.724295 sec
jnh16100850UNSAT657.301079 sec
jnh17100850SAT5.916369 sec
jnh18100850UNSAT6.09238 sec
jnh19100850UNSAT13.556847 sec
jnh1100850SAT7.092443 sec
jnh201100800SAT1.144071 sec
jnh202100800UNSAT0.568035 sec
jnh203100800UNSAT3.924246 sec
jnh204100800SAT1.680105 sec
jnh205100800SAT17.529096 sec
jnh206100800UNSAT3.436216 sec
jnh207100800SAT2.608163 sec
jnh208100800UNSAT10.224639 sec
jnh209100800SAT2.844178 sec
jnh20100850UNSAT6.292393 sec
jnh210100800SAT1.512095 sec
jnh211100800UNSAT2.376149 sec
jnh212100800SAT78.644915 sec
jnh213100800SAT1.416089 sec
jnh214100800UNSAT10.472655 sec
jnh215100800UNSAT3.35221 sec
jnh216100800UNSAT22.473405 sec
jnh217100800SAT3.03219 sec
jnh218100800SAT19.769236 sec
jnh219100800UNSAT126.187887 sec
jnh220100800SAT6.796424 sec
jnh2100850UNSAT1.724108 sec
jnh301100900SAT39.538471 sec
jnh302100900UNSAT0.364023 sec
jnh303100900UNSAT4.564285 sec
jnh304100900UNSAT0.740047 sec
jnh305100900UNSAT0.492031 sec
jnh306100900UNSAT84.685292 sec
jnh307100900UNSAT0.416025 sec
jnh308100900UNSAT2.196137 sec
jnh309100900UNSAT3.092194 sec
jnh310100900UNSAT0.248015 sec
jnh3100850UNSAT18.909182 sec
jnh4100850UNSAT3.704232 sec
jnh5100850UNSAT6.232389 sec
jnh6100850UNSAT58.595662 sec
jnh7100850SAT6.176386 sec
jnh8100850UNSAT1.208076 sec
jnh9100850UNSAT28.00975 sec