 ### SAT solver with ODEs

parent 7d262c89
 /** SAT-solving ODE generation * * run "sat(NbVars, NbClauses), pl2xpp('outfile.ode')." * then call "biocham outfile.ode" and type-in the parameters for clauses * parameter(c_1_1=1, c_1_2=1, c_2_1= -1, c_2_2= -1, c_3_1= -1, c_3_2=1). * numerical_simulation. * plot(show: {x_1, x_2}). * * @author Sylvain Soliman * @license GPL2 */ :- module(satode, [sat/2]). :- reexport(minibiocham). :- use_module(symbolic). %! sat(+N:integer, +M:integer) is det. % % Generates the ODE system for a SAT problem with N variables and M clauses sat(N, M) :- new_ode, forall( between(1, N, I), ( make_name('x', I, Xi), assertz(ode_init(Xi, 0.5)), big_sum(I, M, Gi), assertz(ode_dxdt(Xi, Gi)), make_name('s', I, Si), assertz(ode_func(Si, 2 * Xi - 1)) ) ), forall( between(1, M, J), ( make_name('a', J, Aj), make_name('k', J, Kj), assertz(ode_init(Aj, 1)), assertz(ode_dxdt(Aj, Aj * Kj)), big_prod(J, N, Pj), assertz(ode_func(Kj, Pj / 2^N)) % Could normalize with 2^k for k-SAT ) ), print_xpp. %! make_name(+Prefix:atom, +I:integer, -Name:atom) is det. % % Make a name from a prefix and a number make_name(Prefix, I, Name) :- format(atom(Name), "~w_~d", [Prefix, I]). %! big_prod(+J:integer, +N:integer, -Pj:term) is det. % % Pj is the term corresponding to the prod of all 1 - CjiSi % i.e. unnormalized Kj big_prod(J, N, Pj) :- findall( C, ( between(1, N, I), make_name('c', J, Cj), make_name(Cj, I, Cji), make_name('s', I, Si), C = 1 - Cji * Si ), L ), foldl(prod, L, 1, Pj). prod(X, Y, Y*X). %! big_sum(+I:integer, +M:integer, -Gj:term) is det. % % Gj is the term corresponding to the sum of all AjCjiKjiKj big_sum(I, M, Gi) :- make_name('s', I, Si), findall( C, ( between(1, M, J), make_name('c', J, Cj), make_name(Cj, I, Cji), make_name('a', J, Aj), make_name('k', J, Kj), C = Aj * Cji * Kj^2 / (1 - Cji * Si) ), L ), foldl(sum, L, 0, Gi). sum(X, Y, Y+X).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!